1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro
  5  -/
  6  
  7  import algebra.big_operators algebra.ordered_field
src         └───────────────────┘ └───────────────────┘
  8  
  9  /-!
 10  # Cauchy sequences
 11  
 12  A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where
 13  applicable, lemmas that will be reused in other contexts have been stated in extra generality.
 14  
 15  There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology.
 16  This is a concrete implementation that is useful for simplicity and computability reasons.
 17  
 18  ## Important definitions
 19  
 20  * `is_absolute_value`: a type class stating that `f : β → α` satisfies the axioms of an abs val
 21  * `is_cau_seq`: a predicate that says `f : ℕ → β` is Cauchy.
 22  
 23  ## Tags
 24  
 25  sequence, cauchy, abs val, absolute value
 26  -/
 27  
 28  /-- A function f is an absolute value if it is nonnegative, zero only at 0, additive, and
 29  multiplicative. -/
 30  class is_absolute_value {α} [discrete_linear_ordered_field α]
id                               └───────────────────────────┘ 
src                               └───────────────────────────┘
typ                              └───────────────────────────┘ 
 31    {β} [ring β] (f : β → α) : Prop :=
id         └──┘          
src         └──┘
typ        └──┘          
 32  (abv_nonneg : ∀ x, 0 ≤ f x)
id                         
src                       
typ                        
 33  (abv_eq_zero : ∀ {x}, f x = 0 ↔ x = 0)
id                              
src                                  
typ                             
 34  (abv_add : ∀ x y, f (x + y) ≤ f x + f y)
id                              
src                                  
typ                             
 35  (abv_mul : ∀ x y, f (x * y) = f x * f y)
id                              
src                                  
typ                             
 36  
 37  namespace is_absolute_value
 38  variables {α : Type*} [discrete_linear_ordered_field α]
id                          └───────────────────────────┘
src                         └───────────────────────────┘
typ                         └───────────────────────────┘
 39    {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
id                  └──┘                   └───────────────┘
src                 └──┘                   └───────────────┘
typ                 └──┘                   └───────────────┘
doc                                        └───────────────┘
 40  
 41  theorem abv_zero : abv 0 = 0 := (abv_eq_zero abv).2 rfl
id                      └─┘          └─────────┘ └─┘   └─┘
src                                  └─────────┘       └─┘
typ                     └─┘          └─────────┘ └─┘   └─┘
 42  
 43  theorem abv_one' (h : (1:β) ≠ 0) : abv 1 = 1 :=
id                                    └─┘   
src                                          
typ                                   └─┘   
 44  (domain.mul_left_inj $ mt (abv_eq_zero abv).1 h).1 $
id    └─────────────────┘   └┘  └─────────┘ └─┘    
src   └─────────────────┘   └┘  └─────────┘         
typ   └─────────────────┘   └┘  └─────────┘ └─┘    
doc   └─────────────────┘
 45  by rw [← abv_mul abv, mul_one, mul_one]
id            └─────┘ └─┘  └─────┘  └─────┘
src     └────┘└─────┘   └┘└─────┘└┘└─────┘└─
typ     └────┘└─────┘└─┘└┘└─────┘└┘└─────┘└─
doc     └────┘          └┘       └┘       └─
txt     └────┘          └┘       └┘       └─
par     └────┘          └┘       └┘       └─
pid       └──┘          └┘       └┘       
st     └────────────────┘└───────┘└───────┘
 46  
src  
typ  
doc  
txt  
par  
pid  
st   
 47  theorem abv_one
 48    {β : Type*} [domain β] (abv : β → α) [is_absolute_value abv] :
id                  └────┘                └───────────────┘ └─┘
src                 └────┘                   └───────────────┘
typ                 └────┘                └───────────────┘ └─┘
doc                 └────┘                   └───────────────┘
 49    abv 1 = 1 := abv_one' abv one_ne_zero
id     └─┘         └──────┘ └─┘ └─────────┘
src                └──────┘     └─────────┘
typ    └─┘         └──────┘ └─┘ └─────────┘
 50  
 51  theorem abv_pos {a : β} : 0 < abv a ↔ a ≠ 0 :=
id                               └─┘    
src                                        
typ                              └─┘    
 52  by rw [lt_iff_le_and_ne, ne, eq_comm]; simp [abv_eq_zero abv, abv_nonneg abv]
id          └──────────────┘  └┘  └─────┘         └─────────┘ └─┘  └────────┘ └─┘
src     └──┘└──────────────┘└┘└┘└┘└─────┘  └────┘└─────────┘   └┘└────────┘   └─
typ     └──┘└──────────────┘└┘└┘└┘└─────┘  └────┘└─────────┘└─┘└┘└────────┘└─┘└─
doc     └──┘                └┘  └┘         └────┘              └┘             └─
txt     └──┘                └┘  └┘         └────┘              └┘             └─
par     └──┘                └┘  └┘         └────┘              └┘             └─
pid       └┘                └┘  └┘                           └┘             
st     └───────────────────┘└──┘└───────┘└────────────────────────────────────────
 53  
src  
typ  
doc  
txt  
par  
pid  
st   
 54  theorem abv_neg (a : β) : abv (-a) = abv a :=
id                            └─┘     └─┘ 
src                                    
typ                           └─┘     └─┘ 
 55  by rw [← mul_self_inj_of_nonneg (abv_nonneg abv _) (abv_nonneg abv _),
id            └────────────────────┘                     └────────┘ └─┘
src     └────┘└────────────────────┘              └──┘ └────────┘   └────
typ     └────┘└────────────────────┘              └──┘ └────────┘└─┘└────
doc     └────┘                                    └──┘              └────
txt     └────┘                                    └──┘              └────
par     └────┘                                    └──┘              └────
pid       └──┘                                    └──┘              └────
st     └─────────────────────────────────────────────────────────────────┘└─
 56    ← abv_mul abv, ← abv_mul abv]; simp
id       └─────┘ └─┘    └─────┘ └─┘
src  ───┘└─────┘   └──┘└─────┘     └────
typ  ───┘└─────┘└─┘└──┘└─────┘└─┘  └────
doc  ───┘          └──┘            └────
txt  ───┘          └──┘            └────
par  ───┘          └──┘            └────
pid  ───┘          └──┘                
st   ──────────────┘└─────────────┘└──────
 57  
src  
typ  
doc  
txt  
par  
pid  
st   
 58  theorem abv_sub (a b : β) : abv (a - b) = abv (b - a) :=
id                              └─┘       └─┘    
src                                                 
typ                             └─┘       └─┘    
 59  by rw [← neg_sub, abv_neg abv]
id            └─────┘  └─────┘ └─┘
src     └────┘└─────┘└┘└─────┘   └─
typ     └────┘└─────┘└┘└─────┘└─┘└─
doc     └────┘       └┘          └─
txt     └────┘       └┘          └─
par     └────┘       └┘          └─
pid       └──┘       └┘          
st     └────────────┘└───────────┘
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  theorem abv_inv
 62    {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id                  └────────────┘                └───────────────┘ └─┘
src                 └────────────┘                   └───────────────┘
typ                 └────────────┘                └───────────────┘ └─┘
doc                                                  └───────────────┘
 63    (a : β) : abv a⁻¹ = (abv a)⁻¹ :=
id              └─┘ └┘   └─┘  └┘
src                   └┘         └┘
typ             └─┘ └┘   └─┘  └┘
 64  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
 65    (λ h : a = 0, by simp [h, abv_zero abv])
id                            └──────┘ └─┘
src                    └────┘ └┘└──────┘   
typ                   └────┘└┘└──────┘└─┘
doc                     └────┘ └┘           
txt                     └────┘ └┘           
par                     └────┘ └┘           
pid                          └┘           
st                     └─────────────────────┘
 66    (λ h, (domain.mul_left_inj (mt (abv_eq_zero abv).1 h)).1 $
id           └─────────────────┘  └┘  └─────────┘ └─┘     
src           └─────────────────┘  └┘  └─────────┘          
typ          └─────────────────┘  └┘  └─────────┘ └─┘     
doc           └─────────────────┘
 67      by rw [← abv_mul abv]; simp [h, mt (abv_eq_zero abv).1 h, abv_one abv])
id                └─────┘ └─┘           └┘  └─────────┘ └─┘      └─────┘ └─┘
src         └────┘└─────┘     └────┘ └┘└┘ └─────────┘   └──┘ └┘└─────┘   
typ         └────┘└─────┘└─┘  └────┘└┘└┘ └─────────┘└─┘└──┘└┘└─────┘└─┘
doc         └────┘            └────┘ └┘                 └──┘ └┘          
txt         └────┘            └────┘ └┘                 └──┘ └┘          
par         └────┘            └────┘ └┘                 └──┘ └┘          
pid           └──┘                 └┘                 └──┘ └┘          
st         └────────────────┘└───────────────────────────────────────────────┘
 68  
 69  theorem abv_div
 70    {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id                  └────────────┘                └───────────────┘ └─┘
src                 └────────────┘                   └───────────────┘
typ                 └────────────┘                └───────────────┘ └─┘
doc                                                  └───────────────┘
 71    (a b : β) : abv (a / b) = abv a / abv b :=
id                └─┘       └─┘   └─┘ 
src                                  
typ               └─┘       └─┘   └─┘ 
 72  by rw [division_def, abv_mul abv, abv_inv abv]; refl
id          └──────────┘  └─────┘ └─┘  └─────┘ └─┘
src     └──┘└──────────┘└┘└─────┘   └┘└─────┘     └────
typ     └──┘└──────────┘└┘└─────┘└─┘└┘└─────┘└─┘  └────
doc     └──┘            └┘          └┘            └────
txt     └──┘            └┘          └┘            └────
par     └──┘            └┘          └┘            └────
pid       └┘            └┘          └┘                
st     └───────────────┘└───────────┘└───────────┘└──────
 73  
src  
typ  
doc  
txt  
par  
pid  
st   
 74  lemma abv_sub_le (a b c : β) : abv (a - c) ≤ abv (a - b) + abv (b - c) :=
id                                 └─┘       └─┘       └─┘    
src                                                                
typ                                └─┘       └─┘       └─┘    
 75  by simpa using abv_add abv (a - b) (b - c)
id                  └─────┘ └─┘           
src     └──────────┘└─────┘      └┘    └─
typ     └──────────┘└─────┘└─┘  └┘  └─
doc     └──────────┘              └┘    └─
txt     └──────────┘              └┘    └─
par     └──────────┘              └┘    └─
pid          └────┘              └┘    
st     └────────────────────────────────────────
 76  
src  
typ  
doc  
txt  
par  
pid  
st   
 77  lemma sub_abv_le_abv_sub (a b : β) : abv a - abv b ≤ abv (a - b) :=
id                                       └─┘   └─┘   └─┘    
src                                                            
typ                                      └─┘   └─┘   └─┘    
 78  sub_le_iff_le_add.2 $ by simpa using abv_add abv (a - b) b
id   └───────────────┘                   └─────┘ └─┘       
src  └───────────────┘       └──────────┘└─────┘      └┘ 
typ  └───────────────┘       └──────────┘└─────┘└─┘  └┘
doc                           └──────────┘              └┘ 
txt                           └──────────┘              └┘ 
par                           └──────────┘              └┘ 
pid                                └────┘              └┘ 
st                           └──────────────────────────────────
 79  
src  
typ  
doc  
txt  
par  
pid  
st   
 80  lemma abs_abv_sub_le_abv_sub (a b : β) :
id                                       
typ                                      
 81    abs (abv a - abv b) ≤ abv (a - b) :=
id     └─┘  └─┘   └─┘    └─┘    
src    └─┘                        
typ    └─┘  └─┘   └─┘    └─┘    
 82  abs_sub_le_iff.2 ⟨sub_abv_le_abv_sub abv _ _,
id   └────────────┘   └────────────────┘ └─┘
src  └────────────┘   └────────────────┘
typ  └────────────┘   └────────────────┘ └─┘
 83    by rw abv_sub abv; apply sub_abv_le_abv_sub abv⟩
id           └─────┘ └─┘        └────────────────┘ └─┘
src       └─┘└─────┘     └────┘└────────────────┘
typ       └─┘└─────┘└─┘  └────┘└────────────────┘└─┘
doc       └─┘            └────┘                  
txt       └─┘            └────┘                  
par       └─┘            └────┘                  
pid                                            
st       └───────────────────────────────────────────┘
 84  
 85  lemma abv_pow {β : Type*} [domain β] (abv : β → α) [is_absolute_value abv]
id                              └────┘                └───────────────┘ └─┘
src                             └────┘                   └───────────────┘
typ                             └────┘                └───────────────┘ └─┘
doc                             └────┘                   └───────────────┘
 86    (a : β) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
id                     └─┘       └─┘   
src                                       
typ                    └─┘       └─┘   
 87  by induction n; simp [abv_mul abv, _root_.pow_succ, abv_one abv, *]
id                        └─────┘ └─┘  └─────────────┘  └─────┘ └─┘
src     └────────┘   └────┘└─────┘   └┘└─────────────┘└┘└─────┘   └────
typ     └────────┘  └────┘└─────┘└─┘└┘└─────────────┘└┘└─────┘└─┘└────
doc     └────────┘   └────┘          └┘               └┘          └────
txt     └────────┘   └────┘          └┘               └┘          └────
par     └────────┘   └────┘          └┘               └┘          └────
pid                               └┘               └┘          └──┘
st     └─────────────────────────────────────────────────────────────────
 88  
src  
typ  
doc  
txt  
par  
pid  
st   
 89  end is_absolute_value
 90  
 91  instance abs_is_absolute_value {α} [discrete_linear_ordered_field α] :
id                                       └───────────────────────────┘ 
src                                      └───────────────────────────┘
typ                                      └───────────────────────────┘ 
 92    is_absolute_value (abs : α → α) :=
id     └───────────────┘  └─┘      
src    └───────────────┘  └─┘
typ    └───────────────┘  └─┘      
doc    └───────────────┘
 93  { abv_nonneg  := abs_nonneg,
id                    └────────┘
src                   └────────┘
typ                   └────────┘
 94    abv_eq_zero := λ _, abs_eq_zero,
id                        └─────────┘
src                        └─────────┘
typ                       └─────────┘
 95    abv_add     := abs_add,
id                    └─────┘
src                   └─────┘
typ                   └─────┘
 96    abv_mul     := abs_mul }
id                    └─────┘
src                   └─────┘
typ                   └─────┘
 97  
 98  open is_absolute_value
 99  
100  theorem exists_forall_ge_and {α} [linear_order α] {P Q : α → Prop} :
id                                     └──────────┘          
src                                    └──────────┘
typ                                    └──────────┘          
101    (∃ i, ∀ j ≥ i, P j) → (∃ i, ∀ j ≥ i, Q j) →
id                              
src                          
typ                             
102    ∃ i, ∀ j ≥ i, P j ∧ Q j
id                  
src                    
typ                 
103  | ⟨a, h₁⟩ ⟨b, h₂⟩ := let ⟨c, ac, bc⟩ := exists_ge_of_linear a b in
id        └┘     └┘     └─┘    └┘  └┘     └─────────────────┘
src                                          └─────────────────┘
typ       └┘     └┘     └─┘    └┘  └┘     └─────────────────┘
104    ⟨c, λ j hj, ⟨h₁ _ (le_trans ac hj), h₂ _ (le_trans bc hj)⟩⟩
id            └┘         └──────┘    └┘         └──────┘    └┘
src                       └──────┘               └──────┘
typ           └┘         └──────┘    └┘         └──────┘    └┘
105  
106  section
107  variables {α : Type*} [discrete_linear_ordered_field α]
id                          └───────────────────────────┘
src                         └───────────────────────────┘
typ                         └───────────────────────────┘
108    {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
id                  └──┘                   └───────────────┘
src                 └──┘                   └───────────────┘
typ                 └──┘                   └───────────────┘
doc                                        └───────────────┘
109  
110  theorem rat_add_continuous_lemma
111    {ε : α} (ε0 : 0 < ε) : ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β},
id                                                
src                                
typ                                               
112    abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε :=
id     └─┘  └┘  └┘      └─┘  └┘  └┘      └─┘  └┘  └┘   └┘  └┘    
src                                                               
typ    └─┘  └┘  └┘      └─┘  └┘  └┘      └─┘  └┘  └┘   └┘  └┘    
113  ⟨ε / 2, half_pos ε0, λ a₁ a₂ b₁ b₂ h₁ h₂,
id         └──────┘ └┘    └┘ └┘ └┘ └┘ └┘ └┘
src         └──────┘
typ        └──────┘ └┘    └┘ └┘ └┘ └┘ └┘ └┘
114    by simpa [add_halves] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)⟩
id               └────────┘        └────────────┘  └─────┘ └─┘       └────────┘ └┘ └┘
src       └─────┘└────────┘└──────┘└────────────┘ └─────┘   └────┘ └────────┘    
typ       └─────┘└────────┘└──────┘└────────────┘ └─────┘└─┘└────┘ └────────┘└┘└┘
doc       └─────┘          └──────┘                         └────┘               
txt       └─────┘          └──────┘                         └────┘               
par       └─────┘          └──────┘                         └────┘               
pid                      └────┘                         └────┘               
st       └───────────────────────────────────────────────────────────────────────────┘
115  
116  theorem rat_mul_continuous_lemma
117    {ε K₁ K₂ : α} (ε0 : 0 < ε) :
id                           
src                          
typ                          
118    ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ →
id                               └─┘ └┘  └┘   └─┘ └┘  └┘
src                                                    
typ                              └─┘ └┘  └┘   └─┘ └┘  └┘
119    abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε :=
id     └─┘  └┘  └┘      └─┘  └┘  └┘      └─┘  └┘  └┘  └┘  └┘   
src                                                             
typ    └─┘  └┘  └┘      └─┘  └┘  └┘      └─┘  └┘  └┘  └┘  └┘   
120  begin
st   └─────
121    have K0 : (0 : α) < max 1 (max K₁ K₂) := lt_of_lt_of_le zero_lt_one (le_max_left _ _),
id                              └─┘ └┘ └┘     └────────────┘ └─────────┘  └─────────┘
src    └────────┘ └──┘ └┘   └─┘ └─┘    └───┘└────────────┘└─────────┘ └─────────┘└───┘
typ    └────────┘ └──┘└┘   └─┘ └─┘└┘└┘└───┘└────────────┘└─────────┘ └─────────┘└───┘
doc    └────────┘ └──┘ └┘    └─┘        └───┘                                     └───┘
txt    └────────┘ └──┘ └┘    └─┘        └───┘                                     └───┘
par    └────────┘ └──┘ └┘    └─┘        └───┘                                     └───┘
pid    └─────┘└─┘ └──┘ └┘    └─┘        └──┘                                     └───┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
122    have εK := div_pos (half_pos ε0) K0,
id                └─────┘  └──────┘ └┘  └┘
src    └─────────┘└─────┘ └──────┘  └┘
typ    └─────────┘└─────┘ └──────┘└┘└┘└┘
doc    └─────────┘                  └┘
txt    └─────────┘                  └┘
par    └─────────┘                  └┘
pid    └─────┘└─┘                  └┘
st   ────────────────────────────────────┘└─
123    refine ⟨_, εK, λ a₁ a₂ b₁ b₂ ha₁ hb₂ h₁ h₂, _⟩,
id                └┘
src    └─────┘ └─┘  └┘ └────────────────────────────┘
typ    └─────┘ └─┘└┘└┘ └────────────────────────────┘
doc    └─────┘ └─┘  └┘ └────────────────────────────┘
txt    └─────┘ └─┘  └┘ └────────────────────────────┘
par    └─────┘ └─┘  └┘ └────────────────────────────┘
pid           └─┘  └┘ └────────────────────────────┘
st   ───────────────────────────────────────────────┘└─
124    replace ha₁ := lt_of_lt_of_le ha₁ (le_trans (le_max_left _ K₂) (le_max_right 1 _)),
id                    └────────────┘ └─┘  └──────┘  └─────────┘   └┘   └──────────┘
src    └─────────────┘└────────────┘    └──────┘ └─────────┘└─┘  └┘ └──────────┘└────┘
typ    └─────────────┘└────────────┘└─┘ └──────┘ └─────────┘└─┘└┘└┘ └──────────┘└────┘
doc    └─────────────┘                                      └─┘  └┘             └────┘
txt    └─────────────┘                                      └─┘  └┘             └────┘
par    └─────────────┘                                      └─┘  └┘             └────┘
pid           └──┘└─┘                                      └─┘  └┘             └────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
125    replace hb₂ := lt_of_lt_of_le hb₂ (le_trans (le_max_right K₁ _) (le_max_right 1 _)),
id                    └────────────┘ └─┘  └──────┘               └┘     └──────────┘
src    └─────────────┘└────────────┘    └──────┘               └──┘ └──────────┘└────┘
typ    └─────────────┘└────────────┘└─┘ └──────┘             └┘└──┘ └──────────┘└────┘
doc    └─────────────┘                                         └──┘             └────┘
txt    └─────────────┘                                         └──┘             └────┘
par    └─────────────┘                                         └──┘             └────┘
pid           └──┘└─┘                                         └──┘             └────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
126    have := add_lt_add
id             └────────┘
src    └──────┘└────────┘
typ    └──────┘└────────┘
doc    └──────┘          
txt    └──────┘          
par    └──────┘          
pid    └───┘└─┘          
st   ─────────────────────
127      (mul_lt_mul' (le_of_lt h₁) hb₂ (abv_nonneg abv _) εK)
id                              └┘  └─┘
src  ───┘                       └┘                 └──┘  └─
typ  ───┘                     └┘└┘└─┘              └──┘  └─
doc  ───┘                       └┘                 └──┘  └─
txt  ───┘                       └┘                 └──┘  └─
par  ───┘                       └┘                 └──┘  └─
pid  ───┘                       └┘                 └──┘  └─
st   ──────────────────────────────────────────────────────────
128      (mul_lt_mul' (le_of_lt h₂) ha₁ (abv_nonneg abv _) εK),
id        └─────────┘  └──────┘ └┘  └─┘  └────────┘ └─┘    └┘
src  ───┘ └─────────┘ └──────┘  └┘    └────────┘   └──┘  
typ  ───┘ └─────────┘ └──────┘└┘└┘└─┘ └────────┘└─┘└──┘└┘
doc  ───┘                       └┘                 └──┘  
txt  ───┘                       └┘                 └──┘  
par  ───┘                       └┘                 └──┘  
pid  ───┘                       └┘                 └──┘  
st   ────────────────────────────────────────────────────────┘└─
129    rw [← abv_mul abv, mul_comm, div_mul_cancel _ (ne_of_gt K0), ← abv_mul abv, add_halves] at this,
id           └─────┘ └─┘  └──────┘  └────────────┘    └──────┘ └┘     └─────┘ └─┘  └────────┘
src    └────┘└─────┘   └┘└──────┘└┘└────────────┘└─┘ └──────┘  └───┘└─────┘   └┘└────────┘└───────┘
typ    └────┘└─────┘└─┘└┘└──────┘└┘└────────────┘└─┘ └──────┘└┘└───┘└─────┘└─┘└┘└────────┘└───────┘
doc    └────┘          └┘        └┘              └─┘           └───┘          └┘          └───────┘
txt    └────┘          └┘        └┘              └─┘           └───┘          └┘          └───────┘
par    └────┘          └┘        └┘              └─┘           └───┘          └┘          └───────┘
pid      └──┘          └┘        └┘              └─┘           └───┘          └┘          └──────┘
st   ──────────────────┘└────────┘└──────────────────────────────┘└─────────────┘└──────────┘└──────┘└─
130    simpa [mul_add, add_mul] using lt_of_le_of_lt (abv_add abv _ _) this
id            └─────┘  └─────┘        └────────────┘  └─────┘ └─┘      └──┘
src    └─────┘└─────┘└┘└─────┘└──────┘└────────────┘ └─────┘   └────┘    
typ    └─────┘└─────┘└┘└─────┘└──────┘└────────────┘ └─────┘└─┘└────┘└──┘
doc    └─────┘       └┘       └──────┘                         └────┘    
txt    └─────┘       └┘       └──────┘                         └────┘    
par    └─────┘       └┘       └──────┘                         └────┘    
pid                └┘       └────┘                         └────┘    
st   ──────────────────────────────────────────────────────────────────────┘
131  end
st   └─┘
132  
133  theorem rat_inv_continuous_lemma
134    {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id                  └────────────┘                └───────────────┘ └─┘
src                 └────────────┘                   └───────────────┘
typ                 └────────────┘                └───────────────┘ └─┘
doc                                                  └───────────────┘
135    {ε K : α} (ε0 : 0 < ε) (K0 : 0 < K) :
id                                  
src                                  
typ                                 
136    ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b →
id                         └─┘      └─┘ 
src                                     
typ                        └─┘      └─┘ 
137    abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε :=
id     └─┘          └─┘  └┘  └┘   
src                          └┘   └┘  
typ    └─┘          └─┘  └┘  └┘   
138  begin
st   └─────
139    have KK := mul_pos K0 K0,
id                └─────┘    └┘
src    └─────────┘└─────┘  
typ    └─────────┘└─────┘  └┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid    └─────┘└─┘         
st   ─────────────────────────┘└─
140    have εK := mul_pos ε0 KK,
id                └─────┘ └┘ └┘
src    └─────────┘└─────┘  
typ    └─────────┘└─────┘└┘└┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid    └─────┘└─┘         
st   ─────────────────────────┘└─
141    refine ⟨_, εK, λ a b ha hb h, _⟩,
id                └┘
src    └─────┘ └─┘  └┘ └──────────────┘
typ    └─────┘ └─┘└┘└┘ └──────────────┘
doc    └─────┘ └─┘  └┘ └──────────────┘
txt    └─────┘ └─┘  └┘ └──────────────┘
par    └─────┘ └─┘  └┘ └──────────────┘
pid           └─┘  └┘ └──────────────┘
st   ─────────────────────────────────┘└─
142    have a0 := lt_of_lt_of_le K0 ha,
id                └────────────┘ └┘ └┘
src    └─────────┘└────────────┘  
typ    └─────────┘└────────────┘└┘└┘
doc    └─────────┘                
txt    └─────────┘                
par    └─────────┘                
pid    └─────┘└─┘                
st   ────────────────────────────────┘└─
143    have b0 := lt_of_lt_of_le K0 hb,
id                └────────────┘ └┘ └┘
src    └─────────┘└────────────┘  
typ    └─────────┘└────────────┘└┘└┘
doc    └─────────┘                
txt    └─────────┘                
par    └─────────┘                
pid    └─────┘└─┘                
st   ────────────────────────────────┘└─
144    rw [inv_sub_inv ((abv_pos abv).1 a0) ((abv_pos abv).1 b0),
id         └─────────┘                  └┘    └─────┘ └─┘    └┘
src    └──┘└─────────┘            └──┘  └┘  └─────┘   └──┘  └──
typ    └──┘└─────────┘            └──┘└┘└┘  └─────┘└─┘└──┘└┘└──
doc    └──┘                       └──┘  └┘            └──┘  └──
txt    └──┘                       └──┘  └┘            └──┘  └──
par    └──┘                       └──┘  └┘            └──┘  └──
pid      └┘                       └──┘  └┘            └──┘  └──
st   ──────────────────────────────────────────────────────────┘└─
145        abv_div abv, abv_mul abv, mul_comm, abv_sub abv,
id         └─────┘ └─┘  └─────┘ └─┘  └──────┘  └─────┘ └─┘
src  ─────┘└─────┘   └┘└─────┘   └┘└──────┘└┘└─────┘   └─
typ  ─────┘└─────┘└─┘└┘└─────┘└─┘└┘└──────┘└┘└─────┘└─┘└─
doc  ─────┘          └┘          └┘        └┘          └─
txt  ─────┘          └┘          └┘        └┘          └─
par  ─────┘          └┘          └┘        └┘          └─
pid  ─────┘          └┘          └┘        └┘          └─
st   ────────────────┘└───────────┘└────────┘└───────────┘└─
146        ← mul_div_cancel ε (ne_of_gt KK)],
id           └────────────┘   └──────┘ └┘
src  ───────┘└────────────┘  └──────┘  └┘
typ  ───────┘└────────────┘ └──────┘└┘└┘
doc  ───────┘                          └┘
txt  ───────┘                          └┘
par  ───────┘                          └┘
pid  ───────┘                          └┘
st   ─────────────────────────────────────┘└──
147    exact div_lt_div h
id           └────────┘ 
src    └────┘└────────┘ 
typ    └────┘└────────┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ─────────────────────
148      (mul_le_mul hb ha (le_of_lt K0) (abv_nonneg abv _))
id        └────────┘ └┘ └┘           └┘   └────────┘ └─┘
src  ───┘ └────────┘               └┘ └────────┘   └────
typ  ───┘ └────────┘└┘└┘         └┘└┘ └────────┘└─┘└────
doc  ───┘                          └┘              └────
txt  ───┘                          └┘              └────
par  ───┘                          └┘              └────
pid  ───┘                          └┘              └────
st   ────────────────────────────────────────────────────────
149      (le_of_lt $ mul_pos ε0 KK) KK
id        └──────┘   └─────┘ └┘     └┘
src  ───┘ └──────┘ └─────┘    └┘  
typ  ───┘ └──────┘ └─────┘└┘  └┘└┘
doc  ───┘                     └┘  
txt  ───┘                     └┘  
par  ───┘                     └┘  
pid  ───┘                     └┘  
st   ─────────────────────────────────┘
150  end
st   └─┘
151  end
152  
153  /-- A sequence is Cauchy if the distance between its entries tends to zero. -/
154  def is_cau_seq {α : Type*} [discrete_linear_ordered_field α]
id                               └───────────────────────────┘ 
src                              └───────────────────────────┘
typ                              └───────────────────────────┘ 
155    {β : Type*} [ring β] (abv : β → α) (f : ℕ → β) :=
id                  └──┘                       
src                 └──┘                       
typ                 └──┘                       
156  ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - f i) < ε
id                    └─┘         
src                                     
typ                   └─┘         
157  
158  namespace is_cau_seq
159  variables {α : Type*} [discrete_linear_ordered_field α]
id                          └───────────────────────────┘
src                         └───────────────────────────┘
typ                         └───────────────────────────┘
160    {β : Type*} [ring β] {abv : β → α} [is_absolute_value abv] {f : ℕ → β}
id                  └──┘                   └───────────────┘           
src                 └──┘                   └───────────────┘           
typ                 └──┘                   └───────────────┘           
doc                                        └───────────────┘
161  
162  theorem cauchy₂ (hf : is_cau_seq abv f) {ε:α} (ε0 : ε > 0) :
id                         └────────┘ └─┘               
src                        └────────┘                      
typ                        └────────┘ └─┘               
doc                        └────────┘
163    ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε :=
id               └─┘         
src                                 
typ              └─┘         
164  begin
st   └─────
165    refine (hf _ (half_pos ε0)).imp (λ i hi j k ij ik, _),
id             └┘    └──────┘ └┘
src    └─────┘   └─┘ └──────┘  └─────┘  └─────────────────┘
typ    └─────┘ └┘└─┘ └──────┘└┘└─────┘  └─────────────────┘
doc    └─────┘   └─┘           └─────┘  └─────────────────┘
txt    └─────┘   └─┘           └─────┘  └─────────────────┘
par    └─────┘   └─┘           └─────┘  └─────────────────┘
pid             └─┘           └─────┘  └─────────────────┘
st   ──────────────────────────────────────────────────────┘└─
166    rw ← add_halves ε,
id          └────────┘ 
src    └───┘└────────┘
typ    └───┘└────────┘
doc    └───┘          
txt    └───┘          
par    └───┘          
pid      └─┘          
st   ──────────────────┘└─
167    refine lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) _),
id            └────────────┘  └────────┘ └─┘         └────────┘  └┘   └┘
src    └─────┘└────────────┘ └────────┘   └──────┘ └────────┘   └─┘  └──┘
typ    └─────┘└────────────┘ └────────┘└─┘└──────┘ └────────┘ └┘└─┘└┘└──┘
doc    └─────┘                            └──────┘              └─┘  └──┘
txt    └─────┘                            └──────┘              └─┘  └──┘
par    └─────┘                            └──────┘              └─┘  └──┘
pid                                      └──────┘              └─┘  └──┘
st   ──────────────────────────────────────────────────────────────────────┘└─
168    rw abv_sub abv, exact hi _ ik
id        └─────┘ └─┘        └┘   └┘
src    └─┘└─────┘     └────┘  └─┘  
typ    └─┘└─────┘└─┘  └────┘└┘└─┘└┘
doc    └─┘            └────┘  └─┘  
txt    └─┘            └────┘  └─┘  
par    └─┘            └────┘  └─┘  
pid                         └─┘  
st   ───────────────┘└──────────────┘
169  end
st   └─┘
170  
171  theorem cauchy₃ (hf : is_cau_seq abv f) {ε:α} (ε0 : ε > 0) :
id                         └────────┘ └─┘               
src                        └────────┘                      
typ                        └────────┘ └─┘               
doc                        └────────┘
172    ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε :=
id                     └─┘         
src                                        
typ                    └─┘         
173  let ⟨i, H⟩ := hf.cauchy₂ ε0 in ⟨i, λ j ij k jk, H _ _ (le_trans ij jk) ij⟩
id   └─┘         └┘└──────┘ └┘           └┘  └┘         └──────┘ └┘ └┘  └┘
src                  └──────┘                               └──────┘
typ  └─┘         └┘└──────┘ └┘           └┘  └┘         └──────┘ └┘ └┘  └┘
174  
175  end is_cau_seq
176  
177  def cau_seq {α : Type*} [discrete_linear_ordered_field α]
id                            └───────────────────────────┘ 
src                           └───────────────────────────┘
typ                           └───────────────────────────┘ 
178    (β : Type*) [ring β] (abv : β → α) :=
id                  └──┘             
src                 └──┘
typ                 └──┘             
179  {f : ℕ → β // is_cau_seq abv f}
id             └────────┘ └─┘ 
src              └────────┘
typ            └────────┘ └─┘ 
doc                └────────┘
180  
181  namespace cau_seq
182  variables {α : Type*} [discrete_linear_ordered_field α]
id                         └───────────────────────────┘
src                         └───────────────────────────┘
typ                        └───────────────────────────┘
183  
184  section ring
185  variables {β : Type*} [ring β] {abv : β → α}
id                         └──┘
src                         └──┘
typ                        └──┘
186  
187  instance : has_coe_to_fun (cau_seq β abv) := ⟨_, subtype.val⟩
id              └────────────┘  └─────┘  └─┘         └─────────┘
src             └────────────┘  └─────┘               └─────────┘
typ             └────────────┘  └─────┘  └─┘         └─────────┘
188  
189  @[simp] theorem mk_to_fun (f) (hf : is_cau_seq abv f) :
id                                       └────────┘ └─┘ 
src                                      └────────┘
typ                                      └────────┘ └─┘ 
doc    └──┘                              └────────┘
190    @coe_fn (cau_seq β abv) _ ⟨f, hf⟩ = f := rfl
id      └────┘  └─────┘  └─┘       └┘       └─┘
src     └────┘  └─────┘                        └─┘
typ     └────┘  └─────┘  └─┘       └┘       └─┘
191  
192  theorem ext {f g : cau_seq β abv} (h : ∀ i, f i = g i) : f = g :=
id                      └─────┘  └─┘                     
src                     └─────┘                                
typ                     └─────┘  └─┘                     
193  subtype.eq (funext h)
id   └────────┘  └────┘ 
src  └────────┘  └────┘
typ  └────────┘  └────┘ 
194  
195  theorem is_cau (f : cau_seq β abv) : is_cau_seq abv f := f.2
id                       └─────┘  └─┘    └────────┘ └─┘     
src                      └─────┘          └────────┘           
typ                      └─────┘  └─┘    └────────┘ └─┘     
doc                                       └────────┘
196  
197  theorem cauchy (f : cau_seq β abv) :
id                       └─────┘  └─┘
src                      └─────┘
typ                      └─────┘  └─┘
198    ∀ {ε}, ε > 0 → ∃ i, ∀ j ≥ i, abv (f j - f i) < ε := f.2
id                          └─┘             
src                                                    
typ                         └─┘             
199  
200  def of_eq (f : cau_seq β abv) (g : ℕ → β) (e : ∀ i, f i = g i) : cau_seq β abv :=
id                  └─────┘  └─┘                             └─────┘  └─┘
src                 └─────┘                                         └─────┘
typ                 └─────┘  └─┘                             └─────┘  └─┘
201  ⟨g, λ ε, by rw [show g = f, from (funext e).symm]; exact f.cauchy⟩
id                                └────┘                └──────┘
src              └──┘      └─────┘ └────┘ └─────┘  └────┘└──────┘
typ            └──┘    └─────┘ └────┘└─────┘  └────┘└──────┘
doc              └──┘       └─────┘        └─────┘  └────┘
txt              └──┘       └─────┘        └─────┘  └────┘
par              └──┘       └─────┘        └─────┘  └────┘
pid                └┘       └─────┘        └─────┘       
st              └──────────────────────────────────┘└┘└──────────────┘
202  
203  variable [is_absolute_value abv]
id             └───────────────┘
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
204  
205  theorem cauchy₂ (f : cau_seq β abv) {ε:α} : ε > 0 →
id                        └─────┘  └─┘          
src                       └─────┘                  
typ                       └─────┘  └─┘          
206    ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε := f.2.cauchy₂
id               └─┘              └─────┘
src                                         └─────┘
typ              └─┘              └─────┘
207  
208  theorem cauchy₃ (f : cau_seq β abv) {ε:α} : ε > 0 →
id                        └─────┘  └─┘          
src                       └─────┘                  
typ                       └─────┘  └─┘          
209    ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε := f.2.cauchy₃
id                     └─┘              └─────┘
src                                                └─────┘
typ                    └─┘              └─────┘
210  
211  theorem bounded (f : cau_seq β abv) : ∃ r, ∀ i, abv (f i) < r :=
id                        └─────┘  └─┘          └─┘      
src                       └─────┘                            
typ                       └─────┘  └─┘          └─┘      
212  begin
st   └─────
213    cases f.cauchy zero_lt_one with i h,
id           └──────┘ └─────────┘
src    └────┘└──────┘└─────────┘└───────┘
typ    └────┘└──────┘└─────────┘└───────┘
doc    └────┘                   └───────┘
txt    └────┘                   └───────┘
par    └────┘                   └───────┘
pid                            └───────┘
st   ────────────────────────────────────┘└─
214    let R := (finset.range (i+1)).sum (λ j, abv (f j)),
id               └──────────┘                └─┘  
src    └───────┘ └──────────┘  └──────┘  └──┘      └┘
typ    └───────┘ └──────────┘ └──────┘  └──┘└─┘  └┘
doc    └───────┘ └──────────┘   └──────┘  └──┘      └┘
txt    └───────┘                └──────┘  └──┘      └┘
par    └───────┘                └──────┘  └──┘      └┘
pid    └───┘└─┘                └──────┘  └──┘      └┘
st   ───────────────────────────────────────────────────┘└─
215    have : ∀ j ≤ i, abv (f j) ≤ R,
id                    └─┘        
src    └─────┘ └───┘        └┘ 
typ    └─────┘ └───┘ └─┘  └┘ 
doc    └─────┘ └───┘        └┘ 
txt    └─────┘ └───┘        └┘ 
par    └─────┘ └───┘        └┘ 
pid    └───┘└┘ └───┘        └┘ 
st   ──────────────────────────────┘└─
216    { intros j ij, change (λ j, abv (f j)) j ≤ R,
id                                 └─┘          
src      └─────────┘  └─────┘  └──┘      └─┘  
typ      └─────────┘  └─────┘  └──┘└─┘  └─┘ 
doc      └─────────┘  └─────┘  └──┘      └─┘  
txt      └─────────┘  └─────┘  └──┘      └─┘  
par      └─────────┘  └─────┘  └──┘      └─┘  
pid            └───┘          └──┘      └─┘  
st   ───┘└─────────┘└─────────────────────────────┘└─
217      apply finset.single_le_sum,
id             └──────────────────┘
src      └────┘└──────────────────┘
typ      └────┘└──────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────┘└─
218      { intros, apply abv_nonneg abv },
id                       └────────┘ └─┘
src        └────┘  └────┘└────────┘   
typ        └────┘  └────┘└────────┘└─┘
doc        └────┘  └────┘             
txt        └────┘  └────┘             
par        └────┘  └────┘             
pid                                  
st   ─────┘└────┘└─────────────────────┘└┘
219      { rwa [finset.mem_range, nat.lt_succ_iff] } },
id              └──────────────┘  └─────────────┘
src        └───┘└──────────────┘└┘└─────────────┘└┘
typ        └───┘└──────────────┘└┘└─────────────┘└┘
doc        └───┘                └┘               └┘
txt        └───┘                └┘               └┘
par        └───┘                └┘               └┘
pid           └┘                └┘               
st   ──────────────────────────┘└───────────────┘└──┘
220    refine ⟨R + 1, λ j, _⟩,
id             
src    └─────┘   └──┘ └────┘
typ    └─────┘  └──┘ └────┘
doc    └─────┘   └──┘ └────┘
txt    └─────┘   └──┘ └────┘
par    └─────┘   └──┘ └────┘
pid             └──┘ └────┘
st   ───────────────────────┘└─
221    cases lt_or_le j i with ij ij,
id           └──────┘  
src    └────┘└──────┘  └─────────┘
typ    └────┘└──────┘└─────────┘
doc    └────┘          └─────────┘
txt    └────┘          └─────────┘
par    └────┘          └─────────┘
pid                   └─────────┘
st   ──────────────────────────────┘└─
222    { exact lt_of_le_of_lt (this _ (le_of_lt ij)) (lt_add_one _) },
id             └────────────┘  └──┘    └──────┘ └┘    └────────┘
src      └────┘└────────────┘     └─┘ └──────┘  └─┘ └────────┘└──┘
typ      └────┘└────────────┘ └──┘└─┘ └──────┘└┘└─┘ └────────┘└──┘
doc      └────┘                   └─┘           └─┘           └──┘
txt      └────┘                   └─┘           └─┘           └──┘
par      └────┘                   └─┘           └─┘           └──┘
pid                              └─┘           └─┘           └─┘
st   ───┘└─────────────────────────────────────────────────────────┘└┘
223    { have := lt_of_le_of_lt (abv_add abv _ _)
id               └────────────┘  └─────┘ └─┘
src      └──────┘└────────────┘ └─────┘   └─────
typ      └──────┘└────────────┘ └─────┘└─┘└─────
doc      └──────┘                         └─────
txt      └──────┘                         └─────
par      └──────┘                         └─────
pid      └───┘└─┘                         └─────
st   ─────────────────────────────────────────────
224        (add_lt_add_of_le_of_lt (this _ (le_refl _)) (h _ ij)),
id          └────────────────────┘  └──┘    └─────┘         └┘
src  ─────┘ └────────────────────┘     └─┘ └─────┘└───┘  └─┘  └┘
typ  ─────┘ └────────────────────┘ └──┘└─┘ └─────┘└───┘ └─┘└┘└┘
doc  ─────┘                            └─┘        └───┘  └─┘  └┘
txt  ─────┘                            └─┘        └───┘  └─┘  └┘
par  ─────┘                            └─┘        └───┘  └─┘  └┘
pid  ─────┘                            └─┘        └───┘  └─┘  └┘
st   ───────────────────────────────────────────────────────────┘└─
225      rw [add_sub, add_comm] at this, simpa }
id           └─────┘  └──────┘
src      └──┘└─────┘└┘└──────┘└───────┘  └────┘
typ      └──┘└─────┘└┘└──────┘└───────┘  └────┘
doc      └──┘       └┘        └───────┘  └────┘
txt      └──┘       └┘        └───────┘  └────┘
par      └──┘       └┘        └───────┘  └────┘
pid        └┘       └┘        └──────┘       
st   ──────────────┘└────────┘└──────┘└──────┘└─
226  end
st   ──┘
227  
228  theorem bounded' (f : cau_seq β abv) (x : α) : ∃ r > x, ∀ i, abv (f i) < r :=
id                         └─────┘  └─┘                    └─┘      
src                        └─────┘                                        
typ                        └─────┘  └─┘                    └─┘      
229  let ⟨r, h⟩ := f.bounded in
id   └─┘         └──────┘
src                 └──────┘
typ  └─┘         └──────┘
230  ⟨max r (x+1), lt_of_lt_of_le (lt_add_one _) (le_max_right _ _),
id    └─┘        └────────────┘  └────────┘     └──────────┘
src   └─┘         └────────────┘  └────────┘     └──────────┘
typ   └─┘        └────────────┘  └────────┘     └──────────┘
231    λ i, lt_of_lt_of_le (h i) (le_max_left _ _)⟩
id         └────────────┘       └─────────┘
src         └────────────┘        └─────────┘
typ        └────────────┘       └─────────┘
232  
233  instance : has_add (cau_seq β abv) :=
id              └─────┘  └─────┘  └─┘
src             └─────┘  └─────┘
typ             └─────┘  └─────┘  └─┘
234  ⟨λ f g, ⟨λ i, (f i + g i : β), λ ε ε0,
id                            └┘
src                     
typ                           └┘
235    let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abv ε0,
id     └─┘     └┘  └┘     └──────────────────────┘ └─┘ └┘
src                       └──────────────────────┘
typ    └─┘     └┘  └┘     └──────────────────────┘ └─┘ └┘
236        ⟨i, H⟩ := exists_forall_ge_and (f.cauchy₃ δ0) (g.cauchy₃ δ0) in
id                 └──────────────────┘  └──────┘      └──────┘
src                  └──────────────────┘   └──────┘       └──────┘
typ                └──────────────────┘  └──────┘      └──────┘
237    ⟨i, λ j ij, let ⟨H₁, H₂⟩ := H _ (le_refl _) in Hδ (H₁ _ ij) (H₂ _ ij)⟩⟩⟩
id            └┘  └─┘  └┘  └┘          └─────┘                └┘        └┘
src                                     └─────┘
typ           └┘  └─┘  └┘  └┘          └─────┘                └┘        └┘
238  
239  @[simp] theorem add_apply (f g : cau_seq β abv) (i : ℕ) : (f + g) i = f i + g i := rfl
id                                    └─────┘  └─┘                          └─┘
src                                   └─────┘                                       └─┘
typ                                   └─────┘  └─┘                          └─┘
doc    └──┘
240  
241  variable (abv)
242  
243  /-- The constant Cauchy sequence. -/
244  def const (x : β) : cau_seq β abv :=
id                      └─────┘  └─┘
src                      └─────┘
typ                     └─────┘  └─┘
245  ⟨λ i, x, λ ε ε0, ⟨0, λ j ij, by simpa [abv_zero abv] using ε0⟩⟩
id             └┘         └┘            └──────┘ └─┘        └┘
src                                  └─────┘└──────┘   └──────┘
typ            └┘         └┘     └─────┘└──────┘└─┘└──────┘└┘
doc                                  └─────┘           └──────┘
txt                                  └─────┘           └──────┘
par                                  └─────┘           └──────┘
pid                                                  └────┘
st                                  └────────────────────────────┘
246  
247  variable {abv}
248  
249  local notation `const` := const abv
id                             └───┘
src                            └───┘
typ                            └───┘
doc                            └───┘
250  
251  @[simp] theorem const_apply (x : β) (i : ℕ) : (const x : ℕ → β) i = x := rfl
id                                                └───┘               └─┘
src                                                └───┘                   └─┘
typ                                               └───┘               └─┘
doc    └──┘                                         └───┘
252  
253  theorem const_inj {x y : β} : (const x : cau_seq β abv) = const y ↔ x = y :=
id                                 └───┘    └─────┘  └─┘   └───┘     
src                                 └───┘     └─────┘         └───┘      
typ                                └───┘    └─────┘  └─┘   └───┘     
doc                                 └───┘                      └───┘
254  ⟨λ h, congr_arg (λ f:cau_seq β abv, (f:ℕ→β) 0) h, congr_arg _⟩
id        └───────┘      └─────┘  └─┘            └───────┘
src        └───────┘      └─────┘                     └───────┘
typ       └───────┘      └─────┘  └─┘            └───────┘
255  
256  instance : has_zero (cau_seq β abv) := ⟨const 0⟩
id              └──────┘  └─────┘  └─┘      └───┘
src             └──────┘  └─────┘            └───┘
typ             └──────┘  └─────┘  └─┘      └───┘
doc                                          └───┘
257  instance : has_one (cau_seq β abv) := ⟨const 1⟩
id              └─────┘  └─────┘  └─┘      └───┘
src             └─────┘  └─────┘            └───┘
typ             └─────┘  └─────┘  └─┘      └───┘
doc                                         └───┘
258  instance : inhabited (cau_seq β abv) := ⟨0⟩
id              └───────┘  └─────┘  └─┘
src             └───────┘  └─────┘
typ             └───────┘  └─────┘  └─┘
259  
260  @[simp] theorem zero_apply (i) : (0 : cau_seq β abv) i = 0 := rfl
id                                         └─────┘  └─┘         └─┘
src                                        └─────┘                └─┘
typ                                        └─────┘  └─┘         └─┘
doc    └──┘
261  @[simp] theorem one_apply (i) : (1 : cau_seq β abv) i = 1 := rfl
id                                        └─────┘  └─┘         └─┘
src                                       └─────┘                └─┘
typ                                       └─────┘  └─┘         └─┘
doc    └──┘
262  
263  theorem const_add (x y : β) : const (x + y) = const x + const y :=
id                                └───┘       └───┘   └───┘ 
src                                └───┘         └───┘    └───┘
typ                               └───┘       └───┘   └───┘ 
doc                                └───┘           └───┘     └───┘
264  ext $ λ i, rfl
id   └─┘       └─┘
src  └─┘        └─┘
typ  └─┘       └─┘
265  
266  instance : has_mul (cau_seq β abv) :=
id              └─────┘  └─────┘  └─┘
src             └─────┘  └─────┘
typ             └─────┘  └─────┘  └─┘
267  ⟨λ f g, ⟨λ i, (f i * g i : β), λ ε ε0,
id                            └┘
src                     
typ                           └┘
268    let ⟨F, F0, hF⟩ := f.bounded' 0, ⟨G, G0, hG⟩ := g.bounded' 0,
id     └─┘         └┘     └───────┘            └┘     └───────┘
src                        └───────┘                    └───────┘
typ    └─┘         └┘     └───────┘            └┘     └───────┘
269        ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abv ε0,
id             └┘  └┘     └──────────────────────┘ └─┘ └┘
src                       └──────────────────────┘
typ            └┘  └┘     └──────────────────────┘ └─┘ └┘
270        ⟨i, H⟩ := exists_forall_ge_and (f.cauchy₃ δ0) (g.cauchy₃ δ0) in
id                 └──────────────────┘  └──────┘      └──────┘
src                  └──────────────────┘   └──────┘       └──────┘
typ                └──────────────────┘  └──────┘      └──────┘
271    ⟨i, λ j ij, let ⟨H₁, H₂⟩ := H _ (le_refl _) in
id            └┘  └─┘  └┘  └┘          └─────┘
src                                     └─────┘
typ           └┘  └─┘  └┘  └┘          └─────┘
272      Hδ (hF j) (hG i) (H₁ _ ij) (H₂ _ ij)⟩⟩⟩
id                             └┘        └┘
typ                            └┘        └┘
273  
274  @[simp] theorem mul_apply (f g : cau_seq β abv) (i : ℕ) : (f * g) i = f i * g i := rfl
id                                    └─────┘  └─┘                          └─┘
src                                   └─────┘                                       └─┘
typ                                   └─────┘  └─┘                          └─┘
doc    └──┘
275  
276  theorem const_mul (x y : β) : const (x * y) = const x * const y :=
id                                └───┘       └───┘   └───┘ 
src                                └───┘         └───┘    └───┘
typ                               └───┘       └───┘   └───┘ 
doc                                └───┘           └───┘     └───┘
277  ext $ λ i, rfl
id   └─┘       └─┘
src  └─┘        └─┘
typ  └─┘       └─┘
278  
279  instance : has_neg (cau_seq β abv) :=
id              └─────┘  └─────┘  └─┘
src             └─────┘  └─────┘
typ             └─────┘  └─────┘  └─┘
280  ⟨λ f, of_eq (const (-1) * f) (λ x, -f x) (λ i, by simp)⟩
id        └───┘  └───┘                   
src        └───┘  └───┘                             └──┘
typ       └───┘  └───┘                        └──┘
doc               └───┘                                └──┘
txt                                                    └──┘
par                                                    └──┘
st                                                    └───┘
281  
282  @[simp] theorem neg_apply (f : cau_seq β abv) (i) : (-f) i = -f i := rfl
id                                  └─────┘  └─┘                  └─┘
src                                 └─────┘                            └─┘
typ                                 └─────┘  └─┘                  └─┘
doc    └──┘
283  
284  theorem const_neg (x : β) : const (-x) = -const x :=
id                              └───┘     └───┘ 
src                              └───┘      └───┘
typ                             └───┘     └───┘ 
doc                              └───┘         └───┘
285  ext $ λ i, rfl
id   └─┘       └─┘
src  └─┘        └─┘
typ  └─┘       └─┘
286  
287  instance : ring (cau_seq β abv) :=
id              └──┘  └─────┘  └─┘
src             └──┘  └─────┘
typ             └──┘  └─────┘  └─┘
288  by refine {neg := has_neg.neg, add := (+), zero := 0, mul := (*), one := 1, ..};
id                     └─────────┘                               
src     └─────┘ └─────┘└─────────┘└───────┘└────────────────────┘└───────────────┘
typ     └─────┘ └─────┘└─────────┘└───────┘└────────────────────┘└───────────────┘
doc     └─────┘ └─────┘           └───────┘ └────────────────────┘ └───────────────┘
txt     └─────┘ └─────┘           └───────┘ └────────────────────┘ └───────────────┘
par     └─────┘ └─────┘           └───────┘ └────────────────────┘ └───────────────┘
pid            └─────┘           └───────┘ └────────────────────┘ └───────────────┘
st     └──────────────────────────────────────────────────────────────────────────────
289     { intros, apply ext, simp [mul_add, mul_assoc, add_mul] }
id                      └─┘        └─────┘  └───────┘  └─────┘
src       └────┘  └────┘└─┘  └────┘└─────┘└┘└───────┘└┘└─────┘└┘
typ       └────┘  └────┘└─┘  └────┘└─────┘└┘└───────┘└┘└─────┘└┘
doc       └────┘  └────┘     └────┘       └┘         └┘       └┘
txt       └────┘  └────┘     └────┘       └┘         └┘       └┘
par       └────┘  └────┘     └────┘       └┘         └┘       └┘
pid                                    └┘         └┘       
st   ──┘└──────┘└─────────┘└───────────────────────────────────┘└┘
290  
291  instance {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv] : comm_ring (cau_seq β abv) :=
id                         └───────┘                └───────────────┘ └─┘    └───────┘  └─────┘  └─┘
src                        └───────┘                   └───────────────┘        └───────┘  └─────┘
typ                        └───────┘                └───────────────┘ └─┘    └───────┘  └─────┘  └─┘
doc                                                    └───────────────┘
292  { mul_comm := by intros; apply ext; simp [mul_left_comm, mul_comm],
id                                  └─┘        └───────────┘  └──────┘
src                   └────┘  └────┘└─┘  └────┘└───────────┘└┘└──────┘
typ                   └────┘  └────┘└─┘  └────┘└───────────┘└┘└──────┘
doc                   └────┘  └────┘     └────┘             └┘        
txt                   └────┘  └────┘     └────┘             └┘        
par                   └────┘  └────┘     └────┘             └┘        
pid                                                      └┘        
st                   └────────────────────────────────────────────────┘
293    ..cau_seq.ring }
id       └──────────┘
src      └──────────┘
typ      └──────────┘
294  
295  theorem const_sub (x y : β) : const (x - y) = const x - const y :=
id                                └───┘       └───┘   └───┘ 
src                                └───┘         └───┘    └───┘
typ                               └───┘       └───┘   └───┘ 
doc                                └───┘           └───┘     └───┘
296  by rw [sub_eq_add_neg, const_add, const_neg, sub_eq_add_neg]
id          └────────────┘  └───────┘  └───────┘  └────────────┘
src     └──┘└────────────┘└┘└───────┘└┘└───────┘└┘└────────────┘└─
typ     └──┘└────────────┘└┘└───────┘└┘└───────┘└┘└────────────┘└─
doc     └──┘              └┘         └┘         └┘              └─
txt     └──┘              └┘         └┘         └┘              └─
par     └──┘              └┘         └┘         └┘              └─
pid       └┘              └┘         └┘         └┘              
st     └─────────────────┘└─────────┘└─────────┘└──────────────┘
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  @[simp] theorem sub_apply (f g : cau_seq β abv) (i : ℕ) : (f - g) i = f i - g i := rfl
id                                    └─────┘  └─┘                          └─┘
src                                   └─────┘                                       └─┘
typ                                   └─────┘  └─┘                          └─┘
doc    └──┘
299  
300  /-- `lim_zero f` holds when `f` approaches 0. -/
301  def lim_zero (f : cau_seq β abv) := ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j) < ε
id                     └─────┘  └─┘                      └─┘      
src                    └─────┘                                          
typ                    └─────┘  └─┘                      └─┘      
302  
303  theorem add_lim_zero {f g : cau_seq β abv}
id                               └─────┘  └─┘
src                              └─────┘
typ                              └─────┘  └─┘
304    (hf : lim_zero f) (hg : lim_zero g) : lim_zero (f + g)
id           └──────┘         └──────┘     └──────┘    
src          └──────┘          └──────┘      └──────┘    
typ          └──────┘         └──────┘     └──────┘    
doc          └──────┘          └──────┘      └──────┘
305  | ε ε0 := (exists_forall_ge_and
id       └┘     └──────────────────┘
src             └──────────────────┘
typ      └┘     └──────────────────┘
306      (hf _ $ half_pos ε0) (hg _ $ half_pos ε0)).imp $
id        └┘     └──────┘      └┘     └──────┘     └─┘
src              └──────┘             └──────┘     └─┘
typ       └┘     └──────┘      └┘     └──────┘     └─┘
307    λ i H j ij, let ⟨H₁, H₂⟩ := H _ ij in
id          └┘  └─┘                └┘
typ         └┘  └─┘                └┘
308      by simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)
id                 └────────┘         └────────────┘  └─────┘ └─┘       └────────┘ └┘ └┘
src         └─────┘└────────┘ └──────┘└────────────┘ └─────┘   └────┘ └────────┘    └─
typ         └─────┘└────────┘└──────┘└────────────┘ └─────┘└─┘└────┘ └────────┘└┘└┘└─
doc         └─────┘           └──────┘                         └────┘               └─
txt         └─────┘           └──────┘                         └────┘               └─
par         └─────┘           └──────┘                         └────┘               └─
pid                         └────┘                         └────┘               
st         └───────────────────────────────────────────────────────────────────────────────
309  
src  
typ  
doc  
txt  
par  
pid  
st   
310  theorem mul_lim_zero_right (f : cau_seq β abv) {g}
id                                   └─────┘  └─┘
src                                  └─────┘
typ                                  └─────┘  └─┘
311    (hg : lim_zero g) : lim_zero (f * g)
id           └──────┘     └──────┘    
src          └──────┘      └──────┘    
typ          └──────┘     └──────┘    
doc          └──────┘      └──────┘
312  | ε ε0 := let ⟨F, F0, hF⟩ := f.bounded' 0 in
id       └┘    └─┘     └┘         └───────┘
src                                └───────┘
typ      └┘    └─┘     └┘         └───────┘
313    (hg _ $ div_pos ε0 F0).imp $ λ i H j ij,
id      └┘     └─────┘       └─┘         └┘
src            └─────┘       └─┘
typ     └┘     └─────┘       └─┘         └┘
314    by have := mul_lt_mul' (le_of_lt $ hF j) (H _ ij) (abv_nonneg abv _) F0;
id                └─────────┘  └──────┘   └┘       └┘   └────────┘ └─┘    └┘
src       └──────┘└─────────┘ └──────┘    └┘  └─┘  └┘ └────────┘   └──┘
typ       └──────┘└─────────┘ └──────┘ └┘└┘ └─┘└┘└┘ └────────┘└─┘└──┘└┘
doc       └──────┘                        └┘  └─┘  └┘              └──┘
txt       └──────┘                        └┘  └─┘  └┘              └──┘
par       └──────┘                        └┘  └─┘  └┘              └──┘
pid       └───┘└─┘                        └┘  └─┘  └┘              └──┘
st       └──────────────────────────────────────────────────────────────────────
315       rwa [mul_comm F, div_mul_cancel _ (ne_of_gt F0), ← abv_mul abv] at this
id             └──────┘   └────────────┘    └──────┘ └┘     └─────┘ └─┘
src       └───┘└──────┘ └┘└────────────┘└─┘ └──────┘  └───┘└─────┘   └─────────
typ       └───┘└──────┘└┘└────────────┘└─┘ └──────┘└┘└───┘└─────┘└─┘└─────────
doc       └───┘         └┘              └─┘           └───┘          └─────────
txt       └───┘         └┘              └─┘           └───┘          └─────────
par       └───┘         └┘              └─┘           └───┘          └─────────
pid          └┘         └┘              └─┘           └───┘          └──────┘
st   ─────────┘└────────┘└──────────────────────────────┘└─────────────┘└────────
316  
src  
typ  
doc  
txt  
par  
pid  
st   
317  theorem mul_lim_zero_left {f} (g : cau_seq β abv)
id                                      └─────┘  └─┘
src                                     └─────┘
typ                                     └─────┘  └─┘
318    (hg : lim_zero f) : lim_zero (f * g)
id           └──────┘     └──────┘    
src          └──────┘      └──────┘    
typ          └──────┘     └──────┘    
doc          └──────┘      └──────┘
319  | ε ε0 := let ⟨G, G0, hG⟩ := g.bounded' 0 in
id       └┘    └─┘     └┘         └───────┘
src                                └───────┘
typ      └┘    └─┘     └┘         └───────┘
320    (hg _ $ div_pos ε0 G0).imp $ λ i H j ij,
id      └┘     └─────┘       └─┘         └┘
src            └─────┘       └─┘
typ     └┘     └─────┘       └─┘         └┘
321    by have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _);
id                └──────────┘     └┘   └┘                       └────────┘ └─┘
src       └──────┘└──────────┘  └─┘  └┘    └┘              └──┘ └────────┘   └─┘
typ       └──────┘└──────────┘ └─┘└┘└┘ └┘└┘              └──┘ └────────┘└─┘└─┘
doc       └──────┘              └─┘  └┘    └┘              └──┘              └─┘
txt       └──────┘              └─┘  └┘    └┘              └──┘              └─┘
par       └──────┘              └─┘  └┘    └┘              └──┘              └─┘
pid       └───┘└─┘              └─┘  └┘    └┘              └──┘              └─┘
st       └────────────────────────────────────────────────────────────────────────────
322       rwa [div_mul_cancel _ (ne_of_gt G0), ← abv_mul abv] at this
id             └────────────┘    └──────┘ └┘     └─────┘ └─┘
src       └───┘└────────────┘└─┘ └──────┘  └───┘└─────┘   └─────────
typ       └───┘└────────────┘└─┘ └──────┘└┘└───┘└─────┘└─┘└─────────
doc       └───┘              └─┘           └───┘          └─────────
txt       └───┘              └─┘           └───┘          └─────────
par       └───┘              └─┘           └───┘          └─────────
pid          └┘              └─┘           └───┘          └──────┘
st   ─────────┘└────────────────────────────┘└─────────────┘└────────
323  
src  
typ  
doc  
txt  
par  
pid  
st   
324  theorem neg_lim_zero {f : cau_seq β abv} (hf : lim_zero f) : lim_zero (-f) :=
id                             └─────┘  └─┘        └──────┘     └──────┘  
src                            └─────┘              └──────┘      └──────┘  
typ                            └─────┘  └─┘        └──────┘     └──────┘  
doc                                                 └──────┘      └──────┘
325  by rw ← neg_one_mul; exact mul_lim_zero_right _ hf
id           └─────────┘        └────────────────┘   └┘
src     └───┘└─────────┘  └────┘└────────────────┘└─┘  
typ     └───┘└─────────┘  └────┘└────────────────┘└─┘└┘
doc     └───┘└─────────┘  └────┘                  └─┘  
txt     └───┘             └────┘                  └─┘  
par     └───┘             └────┘                  └─┘  
pid       └─┘                                    └─┘  
st     └────────────────────────────────────────────────
326  
src  
typ  
doc  
txt  
par  
pid  
st   
327  theorem sub_lim_zero {f g : cau_seq β abv}
id                               └─────┘  └─┘
src                              └─────┘
typ                              └─────┘  └─┘
328    (hf : lim_zero f) (hg : lim_zero g) : lim_zero (f - g) :=
id           └──────┘         └──────┘     └──────┘    
src          └──────┘          └──────┘      └──────┘    
typ          └──────┘         └──────┘     └──────┘    
doc          └──────┘          └──────┘      └──────┘
329  add_lim_zero hf (neg_lim_zero hg)
id   └──────────┘ └┘  └──────────┘ └┘
src  └──────────┘     └──────────┘
typ  └──────────┘ └┘  └──────────┘ └┘
330  
331  theorem lim_zero_sub_rev {f g : cau_seq β abv} (hfg : lim_zero (f - g)) : lim_zero (g - f) :=
id                                   └─────┘  └─┘         └──────┘         └──────┘    
src                                  └─────┘               └──────┘           └──────┘    
typ                                  └─────┘  └─┘         └──────┘         └──────┘    
doc                                                        └──────┘            └──────┘
332  by simpa using neg_lim_zero hfg
id                  └──────────┘ └─┘
src     └──────────┘└──────────┘   
typ     └──────────┘└──────────┘└─┘
doc     └──────────┘               
txt     └──────────┘               
par     └──────────┘               
pid          └────┘               
st     └─────────────────────────────
333  
src  
typ  
doc  
txt  
par  
pid  
st   
334  theorem zero_lim_zero : lim_zero (0 : cau_seq β abv)
id                           └──────┘      └─────┘  └─┘
src                          └──────┘      └─────┘
typ                          └──────┘      └─────┘  └─┘
doc                          └──────┘
335  | ε ε0 := ⟨0, λ j ij, by simpa [abv_zero abv] using ε0⟩
id                    └┘            └──────┘ └─┘        └┘
src                           └─────┘└──────┘   └──────┘
typ                   └┘     └─────┘└──────┘└─┘└──────┘└┘
doc                           └─────┘           └──────┘
txt                           └─────┘           └──────┘
par                           └─────┘           └──────┘
pid                                           └────┘
st                           └────────────────────────────┘
336  
337  theorem const_lim_zero {x : β} : lim_zero (const x) ↔ x = 0 :=
id                                   └──────┘  └───┘     
src                                   └──────┘  └───┘       
typ                                  └──────┘  └───┘     
doc                                   └──────┘  └───┘
338  ⟨λ H, (abv_eq_zero abv).1 $
id         └─────────┘ └─┘ 
src         └─────────┘     
typ        └─────────┘ └─┘ 
339    eq_of_le_of_forall_le_of_dense (abv_nonneg abv _) $
id     └────────────────────────────┘  └────────┘ └─┘
src    └────────────────────────────┘  └────────┘
typ    └────────────────────────────┘  └────────┘ └─┘
340    λ ε ε0, let ⟨i, hi⟩ := H _ ε0 in le_of_lt $ hi _ (le_refl _),
id        └┘  └─┘     └┘        └┘    └──────┘         └─────┘
src                                     └──────┘         └─────┘
typ       └┘  └─┘     └┘        └┘    └──────┘         └─────┘
341  λ e, e.symm ▸ zero_lim_zero⟩
id       └───┘  └───────────┘
src        └───┘  └───────────┘
typ      └───┘  └───────────┘
342  
343  instance equiv : setoid (cau_seq β abv) :=
id                    └────┘  └─────┘  └─┘
src                   └────┘  └─────┘
typ                   └────┘  └─────┘  └─┘
344  ⟨λ f g, lim_zero (f - g),
id         └──────┘    
src          └──────┘    
typ        └──────┘    
doc          └──────┘
345  ⟨λ f, by simp [zero_lim_zero],
id                 └───────────┘
src           └────┘└───────────┘
typ          └────┘└───────────┘
doc           └────┘             
txt           └────┘             
par           └────┘             
pid                            
st           └───────────────────┘
346   λ f g h, by simpa using neg_lim_zero h,
id                         └──────────┘ 
src               └──────────┘└──────────┘
typ            └──────────┘└──────────┘
doc               └──────────┘            
txt               └──────────┘            
par               └──────────┘            
pid                    └────┘            
st               └─────────────────────────┘
347   λ f g h fg gh, by simpa using add_lim_zero fg gh⟩⟩
id         └┘ └┘                 └──────────┘ └┘ └┘
src                     └──────────┘└──────────┘  
typ        └┘ └┘     └──────────┘└──────────┘└┘└┘
doc                     └──────────┘              
txt                     └──────────┘              
par                     └──────────┘              
pid                          └────┘              
st                     └─────────────────────────────┘
348  
349  theorem equiv_def₃ {f g : cau_seq β abv} (h : f ≈ g) {ε:α} (ε0 : 0 < ε) :
id                             └─────┘  └─┘                         
src                            └─────┘                                 
typ                            └─────┘  └─┘                         
350    ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
id                     └─┘         
src                                        
typ                    └─┘         
351  (exists_forall_ge_and (h _ $ half_pos ε0) (f.cauchy₃ $ half_pos ε0)).imp $
id    └──────────────────┘       └──────┘ └┘   └──────┘   └──────┘ └┘  └─┘
src   └──────────────────┘        └──────┘       └──────┘   └──────┘     └─┘
typ   └──────────────────┘       └──────┘ └┘   └──────┘   └──────┘ └┘  └─┘
352  λ i H j ij k jk, let ⟨h₁, h₂⟩ := H _ ij in
id        └┘  └┘  └─┘                └┘
typ       └┘  └┘  └─┘                └┘
353  by have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk));
id              └────────────┘  └─────┘ └─┘             └────────┘ └┘  └┘   └┘
src     └──────┘└────────────┘ └─────┘        └───┘ └────────┘     └─┘  └┘
typ     └──────┘└────────────┘ └─────┘└─┘  └───┘ └────────┘└┘ └┘└─┘└┘└┘
doc     └──────┘                               └───┘                └─┘  └┘
txt     └──────┘                               └───┘                └─┘  └┘
par     └──────┘                               └───┘                └─┘  └┘
pid     └───┘└─┘                               └───┘                └─┘  └┘
st     └──────────────────────────────────────────────────────────────────────────────
354     rwa [sub_add_sub_cancel', add_halves] at this
id           └─────────────────┘  └────────┘
src     └───┘└─────────────────┘└┘└────────┘└─────────
typ     └───┘└─────────────────┘└┘└────────┘└─────────
doc     └───┘                   └┘          └─────────
txt     └───┘                   └┘          └─────────
par     └───┘                   └┘          └─────────
pid        └┘                   └┘          └──────┘
st   ───────┘└─────────────────┘└──────────┘└────────
355  
src  
typ  
doc  
txt  
par  
pid  
st   
356  theorem lim_zero_congr {f g : cau_seq β abv} (h : f ≈ g) : lim_zero f ↔ lim_zero g :=
id                                 └─────┘  └─┘             └──────┘   └──────┘ 
src                                └─────┘                     └──────┘    └──────┘
typ                                └─────┘  └─┘             └──────┘   └──────┘ 
doc                                                             └──────┘     └──────┘
357  ⟨λ l, by simpa using add_lim_zero (setoid.symm h) l,
id                       └──────────┘  └─────────┘   
src           └──────────┘└──────────┘ └─────────┘ └┘
typ          └──────────┘└──────────┘ └─────────┘└┘
doc           └──────────┘                         └┘
txt           └──────────┘                         └┘
par           └──────────┘                         └┘
pid                └────┘                         └┘
st           └─────────────────────────────────────────┘
358   λ l, by simpa using add_lim_zero h l⟩
id                       └──────────┘  
src           └──────────┘└──────────┘ 
typ          └──────────┘└──────────┘
doc           └──────────┘             
txt           └──────────┘             
par           └──────────┘             
pid                └────┘             
st           └───────────────────────────┘
359  
360  theorem abv_pos_of_not_lim_zero {f : cau_seq β abv} (hf : ¬ lim_zero f) :
id                                        └─────┘  └─┘         └──────┘ 
src                                       └─────┘               └──────┘
typ                                       └─────┘  └─┘         └──────┘ 
doc                                                              └──────┘
361    ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (f j) :=
id                      └─┘   
src                         
typ                     └─┘   
362  begin
st   └─────
363    haveI := classical.prop_decidable,
id              └──────────────────────┘
src    └───────┘└──────────────────────┘
typ    └───────┘└──────────────────────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ──────────────────────────────────┘└─
364    by_contra nk,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid             └─┘
st   ─────────────┘└─
365    refine hf (λ ε ε0, _),
id            └┘
src    └─────┘    └───────┘
typ    └─────┘└┘  └───────┘
doc    └─────┘    └───────┘
txt    └─────┘    └───────┘
par    └─────┘    └───────┘
pid              └───────┘
st   ──────────────────────┘└─
366    simp [not_forall] at nk,
id           └────────┘
src    └────┘└────────┘└─────┘
typ    └────┘└────────┘└─────┘
doc    └────┘          └─────┘
txt    └────┘          └─────┘
par    └────┘          └─────┘
pid                  └───┘
st   ────────────────────────┘└─
367    cases f.cauchy₃ (half_pos ε0) with i hi,
id           └───────┘  └──────┘ └┘
src    └────┘└───────┘ └──────┘  └─────────┘
typ    └────┘└───────┘ └──────┘└┘└─────────┘
doc    └────┘                    └─────────┘
txt    └────┘                    └─────────┘
par    └────┘                    └─────────┘
pid                             └────────┘
st   ────────────────────────────────────────┘└─
368    rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩,
id            └┘    └──────┘ └┘  
src    └─────┘  └─┘ └──────┘  └┘ └───────────────┘
typ    └─────┘└┘└─┘ └──────┘└┘└┘└───────────────┘
doc    └─────┘  └─┘           └┘ └───────────────┘
txt    └─────┘  └─┘           └┘ └───────────────┘
par    └─────┘  └─┘           └┘ └───────────────┘
pid            └─┘           └┘ └───────────────┘
st   ─────────────────────────────────────────────┘└─
369    refine ⟨j, λ k jk, _⟩,
id             
src    └─────┘  └┘ └───────┘
typ    └─────┘ └┘ └───────┘
doc    └─────┘  └┘ └───────┘
txt    └─────┘  └┘ └───────┘
par    └─────┘  └┘ └───────┘
pid            └┘ └───────┘
st   ──────────────────────┘└─
370    have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj),
id             └────────────┘  └─────┘ └─┘       └────────┘  └┘  └┘  └┘  └┘
src    └──────┘└────────────┘ └─────┘   └────┘ └────────┘         └┘  
typ    └──────┘└────────────┘ └─────┘└─┘└────┘ └────────┘ └┘└┘└┘└┘└┘
doc    └──────┘                         └────┘                    └┘  
txt    └──────┘                         └────┘                    └┘  
par    └──────┘                         └────┘                    └┘  
pid    └───┘└─┘                         └────┘                    └┘  
st   ────────────────────────────────────────────────────────────────────────┘└─
371    rwa [sub_add_cancel, add_halves] at this
id          └────────────┘  └────────┘
src    └───┘└────────────┘└┘└────────┘└────────┘
typ    └───┘└────────────┘└┘└────────┘└────────┘
doc    └───┘              └┘          └────────┘
txt    └───┘              └┘          └────────┘
par    └───┘              └┘          └────────┘
pid       └┘              └┘          └──────┘
st   ────────────────────┘└──────────┘└───────┘
372  end
st   └─┘
373  
374  theorem of_near (f : ℕ → β) (g : cau_seq β abv)
id                                  └─────┘  └─┘
src                                  └─────┘
typ                                 └─────┘  └─┘
375    (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - g j) < ε) : is_cau_seq abv f
id                           └─┘             └────────┘ └─┘ 
src                                                   └────────┘
typ                          └─┘             └────────┘ └─┘ 
doc                                                       └────────┘
376  | ε ε0 :=
id       └┘
typ      └┘
377    let ⟨i, hi⟩ := exists_forall_ge_and
id     └─┘           └──────────────────┘
src                   └──────────────────┘
typ    └─┘           └──────────────────┘
378      (h _ (half_pos $ half_pos ε0)) (g.cauchy₃ $ half_pos ε0) in
id            └──────┘   └──────┘       └──────┘   └──────┘
src            └──────┘   └──────┘        └──────┘   └──────┘
typ           └──────┘   └──────┘       └──────┘   └──────┘
379    ⟨i, λ j ij, begin
id            └┘
typ           └┘
st                 └─────
380      cases hi _ (le_refl _) with h₁ h₂, rw abv_sub abv at h₁,
id             └┘    └─────┘                   └─────┘ └─┘
src      └────┘  └─┘ └─────┘└────────────┘  └─┘└─────┘   └────┘
typ      └────┘└┘└─┘ └─────┘└────────────┘  └─┘└─────┘└─┘└────┘
doc      └────┘  └─┘        └────────────┘  └─┘          └────┘
txt      └────┘  └─┘        └────────────┘  └─┘          └────┘
par      └────┘  └─┘        └────────────┘  └─┘          └────┘
pid             └─┘        └─┘└─────────┘              └────┘
st   ────────────────────────────────────┘└────────────────────┘└─
381      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁),
id               └────────────┘  └─────┘ └─┘       └────────┘  └┘   └┘    └┘
src      └──────┘└────────────┘ └─────┘   └────┘ └────────┘   └─┘  └──┘  
typ      └──────┘└────────────┘ └─────┘└─┘└────┘ └────────┘ └┘└─┘└┘└──┘└┘
doc      └──────┘                         └────┘              └─┘  └──┘  
txt      └──────┘                         └────┘              └─┘  └──┘  
par      └──────┘                         └────┘              └─┘  └──┘  
pid      └───┘└─┘                         └────┘              └─┘  └──┘  
st   ───────────────────────────────────────────────────────────────────────┘└─
382      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij)),
id               └────────────┘  └─────┘ └─┘       └────────┘ └──┘  └┘   └┘
src      └──────┘└────────────┘ └─────┘   └────┘ └────────┘       └─┘  └┘
typ      └──────┘└────────────┘ └─────┘└─┘└────┘ └────────┘└──┘ └┘└─┘└┘└┘
doc      └──────┘                         └────┘                  └─┘  └┘
txt      └──────┘                         └────┘                  └─┘  └┘
par      └──────┘                         └────┘                  └─┘  └┘
pid      └───┘└─┘                         └────┘                  └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
383      rwa [add_halves, add_halves, add_right_comm,
id            └────────┘  └────────┘  └────────────┘
src      └───┘└────────┘└┘└────────┘└┘└────────────┘└─
typ      └───┘└────────┘└┘└────────┘└┘└────────────┘└─
doc      └───┘          └┘          └┘              └─
txt      └───┘          └┘          └┘              └─
par      └───┘          └┘          └┘              └─
pid         └┘          └┘          └┘              └─
st   ──────────────────┘└──────────┘└──────────────┘└─
384           sub_add_sub_cancel, sub_add_sub_cancel] at this
id            └────────────────┘  └────────────────┘
src  ────────┘└────────────────┘└┘└────────────────┘└─────────
typ  ────────┘└────────────────┘└┘└────────────────┘└─────────
doc  ────────┘                  └┘                  └─────────
txt  ────────┘                  └┘                  └─────────
par  ────────┘                  └┘                  └─────────
pid  ────────┘                  └┘                  └──────┘
st   ──────────────────────────┘└──────────────────┘└────────
385    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
386  
387  lemma not_lim_zero_of_not_congr_zero {f : cau_seq _ abv} (hf : ¬ f ≈ 0) : ¬ lim_zero f :=
id                                             └─────┘   └─┘                 └──────┘ 
src                                            └─────┘                        └──────┘
typ                                            └─────┘   └─┘                 └──────┘ 
doc                                                                              └──────┘
388  assume : lim_zero f,
id            └──────┘ 
src           └──────┘
typ           └──────┘ 
doc           └──────┘
389  have lim_zero (f - 0), by simpa,
id        └──────┘   
src       └──────┘            └───┘
typ       └──────┘           └───┘
doc       └──────┘             └───┘
txt                            └───┘
par                            └───┘
st                            └────┘
390  hf this
id   └┘ └──┘
typ  └┘ └──┘
391  
392  lemma mul_equiv_zero  (g : cau_seq _ abv) {f : cau_seq _ abv} (hf : f ≈ 0) : g * f ≈ 0 :=
id                              └─────┘   └─┘       └─────┘   └─┘                  
src                             └─────┘             └─────┘                           
typ                             └─────┘   └─┘       └─────┘   └─┘                  
393  have lim_zero (f - 0), from hf,
id        └──────┘             └┘
src       └──────┘    
typ       └──────┘             └┘
doc       └──────┘
394  have lim_zero (g*f), from mul_lim_zero_right _ $ by simpa,
id        └──────┘          └────────────────┘
src       └──────┘            └────────────────┘        └───┘
typ       └──────┘          └────────────────┘        └───┘
doc       └──────┘                                       └───┘
txt                                                      └───┘
par                                                      └───┘
st                                                      └────┘
395  show lim_zero (g*f - 0), by simpa
id        └──────┘   
src       └──────┘             └─────
typ       └──────┘           └─────
doc       └──────┘               └─────
txt                              └─────
par                              └─────
pid                                   
st                              └──────
396  
src  
typ  
doc  
txt  
par  
pid  
st   
397  lemma mul_not_equiv_zero {f g : cau_seq _ abv} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) : ¬ (f * g) ≈ 0 :=
id                                   └─────┘   └─┘                                  
src                                  └─────┘                                            
typ                                  └─────┘   └─┘                                  
398  assume : lim_zero (f*g - 0),
id            └──────┘   
src           └──────┘     
typ           └──────┘   
doc           └──────┘
399  have hlz : lim_zero (f*g), by simpa,
id              └──────┘  
src             └──────┘          └───┘
typ             └──────┘        └───┘
doc             └──────┘           └───┘
txt                                └───┘
par                                └───┘
st                                └────┘
400  have hf' : ¬ lim_zero f, by simpa using (show ¬ lim_zero (f - 0), from hf),
id               └──────┘                         └──────┘             └┘
src              └──────┘       └──────────┘      └──────┘  └────────┘  
typ              └──────┘      └──────────┘     └──────┘ └────────┘└┘
doc               └──────┘       └──────────┘      └──────┘   └────────┘  
txt                              └──────────┘                 └────────┘  
par                              └──────────┘                 └────────┘  
pid                                   └────┘                 └────────┘  
st                              └─────────────────────────────────────────────┘
401  have hg' : ¬ lim_zero g, by simpa using (show ¬ lim_zero (g - 0), from hg),
id               └──────┘                         └──────┘              └┘
src              └──────┘       └──────────┘      └──────┘   └────────┘  
typ              └──────┘      └──────────┘     └──────┘  └────────┘└┘
doc               └──────┘       └──────────┘      └──────┘   └────────┘  
txt                              └──────────┘                 └────────┘  
par                              └──────────┘                 └────────┘  
pid                                   └────┘                 └────────┘  
st                              └─────────────────────────────────────────────┘
402  begin
st   └─────
403    rcases abv_pos_of_not_lim_zero hf' with ⟨a1, ha1, N1, hN1⟩,
id            └─────────────────────┘ └─┘
src    └─────┘└─────────────────────┘   └──────────────────────┘
typ    └─────┘└─────────────────────┘└─┘└──────────────────────┘
doc    └─────┘                          └──────────────────────┘
txt    └─────┘                          └──────────────────────┘
par    └─────┘                          └──────────────────────┘
pid                                    └──────────────────────┘
st   ───────────────────────────────────────────────────────────┘└─
404    rcases abv_pos_of_not_lim_zero hg' with ⟨a2, ha2, N2, hN2⟩,
id            └─────────────────────┘ └─┘
src    └─────┘└─────────────────────┘   └──────────────────────┘
typ    └─────┘└─────────────────────┘└─┘└──────────────────────┘
doc    └─────┘                          └──────────────────────┘
txt    └─────┘                          └──────────────────────┘
par    └─────┘                          └──────────────────────┘
pid                                    └──────────────────────┘
st   ───────────────────────────────────────────────────────────┘└─
405    have : a1 * a2 > 0, from mul_pos ha1 ha2,
id            └┘  └┘          └─────┘ └─┘ └─┘
src    └─────┘    └┘  └───┘└─────┘   
typ    └─────┘└┘└┘└┘  └───┘└─────┘└─┘└─┘
doc    └─────┘      └┘  └───┘          
txt    └─────┘      └┘  └───┘          
par    └─────┘      └┘  └───┘          
pid    └───┘└┘        └───┘          
st   ───────────────────┘└────────────────────┘└─
406    cases hlz _ this with N hN,
id           └─┘   └──┘
src    └────┘   └─┘    └────────┘
typ    └────┘└─┘└─┘└──┘└────────┘
doc    └────┘   └─┘    └────────┘
txt    └────┘   └─┘    └────────┘
par    └────┘   └─┘    └────────┘
pid            └─┘    └────────┘
st   ───────────────────────────┘└─
407    let i := max N (max N1 N2),
id                    └─┘ └┘ └┘
src    └───────┘     └─┘    
typ    └───────┘    └─┘└┘└┘
doc    └───────┘            
txt    └───────┘            
par    └───────┘            
pid    └───┘└─┘            
st   ───────────────────────────┘└─
408    have hN' := hN i (le_max_left _ _),
id                 └┘   └─────────┘
src    └──────────┘    └─────────┘└───┘
typ    └──────────┘└┘ └─────────┘└───┘
doc    └──────────┘               └───┘
txt    └──────────┘               └───┘
par    └──────────┘               └───┘
pid    └──────┘└─┘               └───┘
st   ───────────────────────────────────┘└─
409    have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _)),
id                  └─┘   └──────┘  └─────────┘       └──────────┘
src    └───────────┘     └──────┘ └─────────┘└────┘ └──────────┘└────┘
typ    └───────────┘└─┘ └──────┘ └─────────┘└────┘ └──────────┘└────┘
doc    └───────────┘                         └────┘             └────┘
txt    └───────────┘                         └────┘             └────┘
par    └───────────┘                         └────┘             └────┘
pid    └───────┘└─┘                         └────┘             └────┘
st   ───────────────────────────────────────────────────────────────────┘└─
410    have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _)),
id                  └─┘   └──────┘                     └──────────┘
src    └───────────┘     └──────┘             └────┘ └──────────┘└────┘
typ    └───────────┘└─┘ └──────┘             └────┘ └──────────┘└────┘
doc    └───────────┘                          └────┘             └────┘
txt    └───────────┘                          └────┘             └────┘
par    └───────────┘                          └────┘             └────┘
pid    └───────┘└─┘                          └────┘             └────┘
st   ────────────────────────────────────────────────────────────────────┘└─
411    apply not_le_of_lt hN',
id           └──────────┘ └─┘
src    └────┘└──────────┘
typ    └────┘└──────────┘└─┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ───────────────────────┘└─
412    change _ ≤ abv (_ * _),
id               └─┘
src    └───────┘    └┘ └─┘
typ    └───────┘└─┘ └┘ └─┘
doc    └───────┘     └┘ └─┘
txt    └───────┘     └┘ └─┘
par    └───────┘     └┘ └─┘
pid          └─┘     └┘ └─┘
st   ───────────────────────┘└─
413    rw is_absolute_value.abv_mul abv,
id        └───────────────────────┘ └─┘
src    └─┘└───────────────────────┘
typ    └─┘└───────────────────────┘└─┘
doc    └─┘                         
txt    └─┘                         
par    └─┘                         
pid                               
st   ─────────────────────────────────┘└─
414    apply mul_le_mul; try { assumption },
id           └────────┘
src    └────┘└────────┘  └────┘└─────────┘
typ    └────┘└────────┘  └────┘└─────────┘
doc    └────┘            └────┘└─────────┘
txt    └────┘            └────┘└─────────┘
par    └────┘            └────┘└─────────┘
pid                        └─────────────┘
st   ────────────────────────┘└──────────┘└┘
415      { apply le_of_lt ha2 },
id               └──────┘ └─┘
src        └────┘└──────┘   
typ        └────┘└──────┘└─┘
doc        └────┘           
txt        └────┘           
par        └────┘           
pid                        
st   ─────┘└─────────────────┘└┘
416      { apply is_absolute_value.abv_nonneg abv }
id               └──────────────────────────┘ └─┘
src        └────┘└──────────────────────────┘   
typ        └────┘└──────────────────────────┘└─┘
doc        └────┘                               
txt        └────┘                               
par        └────┘                               
pid                                            
st   ────────────────────────────────────────────┘└─
417  end
st   ──┘
418  
419  theorem const_equiv {x y : β} : const x ≈ const y ↔ x = y :=
id                                  └───┘   └───┘     
src                                  └───┘    └───┘      
typ                                 └───┘   └───┘     
doc                                  └───┘     └───┘
420  show lim_zero _ ↔ _, by rw [← const_sub, const_lim_zero, sub_eq_zero]
id        └──────┘                └───────┘  └────────────┘  └─────────┘
src       └──────┘          └────┘└───────┘└┘└────────────┘└┘└─────────┘└─
typ       └──────┘          └────┘└───────┘└┘└────────────┘└┘└─────────┘└─
doc       └──────┘           └────┘         └┘              └┘           └─
txt                          └────┘         └┘              └┘           └─
par                          └────┘         └┘              └┘           └─
pid                            └──┘         └┘              └┘           
st                          └──────────────┘└──────────────┘└───────────┘
421  
src  
typ  
doc  
txt  
par  
pid  
st   
422  end ring
423  
424  section comm_ring
425  variables {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
id                          └───────┘                   └───────────────┘
src                         └───────┘                   └───────────────┘
typ                         └───────┘                   └───────────────┘
doc                                                     └───────────────┘
426  
427  lemma mul_equiv_zero' (g : cau_seq _ abv) {f : cau_seq _ abv} (hf : f ≈ 0) : f * g ≈ 0 :=
id                              └─────┘   └─┘       └─────┘   └─┘                  
src                             └─────┘             └─────┘                           
typ                             └─────┘   └─┘       └─────┘   └─┘                  
428  by rw mul_comm; apply mul_equiv_zero _ hf
id         └──────┘        └────────────┘   └┘
src     └─┘└──────┘  └────┘└────────────┘└─┘  
typ     └─┘└──────┘  └────┘└────────────┘└─┘└┘
doc     └─┘          └────┘              └─┘  
txt     └─┘          └────┘              └─┘  
par     └─┘          └────┘              └─┘  
pid                                    └─┘  
st     └───────────────────────────────────────
429  
src  
typ  
doc  
txt  
par  
pid  
st   
430  end comm_ring
431  
432  section integral_domain
433  variables {β : Type*} [integral_domain β] (abv : β → α) [is_absolute_value abv]
id                          └─────────────┘                   └───────────────┘
src                         └─────────────┘                   └───────────────┘
typ                         └─────────────┘                   └───────────────┘
doc                                                           └───────────────┘
434  
435  lemma one_not_equiv_zero : ¬ (const abv 1) ≈ (const abv 0) :=
id                                └───┘ └─┘      └───┘ └─┘
src                               └───┘          └───┘
typ                               └───┘ └─┘      └───┘ └─┘
doc                                └───┘           └───┘
436  assume h,
id          
typ         
437  have ∀ ε > 0, ∃ i, ∀ k, k ≥ i → abv (1 - 0) < ε, from h,
id                           └─┘                
src                                          
typ                          └─┘                
438  have h1 : abv 1 ≤ 0, from le_of_not_gt $
id             └─┘            └──────────┘
src                           └──────────┘
typ            └─┘            └──────────┘
439    assume h2 : abv 1 > 0,
id                 └─┘   
src                      
typ                └─┘   
440    exists.elim (this _ h2) $ λ i hi,
id     └─────────┘  └──┘   └┘       └┘
src    └─────────┘
typ    └─────────┘  └──┘   └┘       └┘
441      lt_irrefl (abv 1) $ by simpa using hi _ (le_refl _),
id       └───────┘  └─┘                     └┘    └─────┘
src      └───────┘              └──────────┘  └─┘ └─────┘└─┘
typ      └───────┘  └─┘         └──────────┘└┘└─┘ └─────┘└─┘
doc                             └──────────┘  └─┘        └─┘
txt                             └──────────┘  └─┘        └─┘
par                             └──────────┘  └─┘        └─┘
pid                                  └────┘  └─┘        └─┘
st                             └───────────────────────────┘
442  have h2 : abv 1 ≥ 0, from is_absolute_value.abv_nonneg _ _,
id             └─┘            └──────────────────────────┘
src                           └──────────────────────────┘
typ            └─┘            └──────────────────────────┘
443  have abv 1 = 0, from le_antisymm h1 h2,
id        └─┘            └─────────┘ └┘ └┘
src                      └─────────┘
typ       └─┘            └─────────┘ └┘ └┘
444  have (1 : β) = 0, from (is_absolute_value.abv_eq_zero abv).1 this,
id                         └───────────────────────────┘ └─┘   └──┘
src                         └───────────────────────────┘     
typ                        └───────────────────────────┘ └─┘   └──┘
445  absurd this one_ne_zero
id   └────┘ └──┘ └─────────┘
src  └────┘      └─────────┘
typ  └────┘ └──┘ └─────────┘
446  
447  end integral_domain
448  
449  section discrete_field
450  variables {β : Type*} [discrete_field β] {abv : β → α} [is_absolute_value abv]
id                          └────────────┘                   └───────────────┘
src                         └────────────┘                   └───────────────┘
typ                         └────────────┘                   └───────────────┘
doc                                                          └───────────────┘
451  
452  theorem inv_aux {f : cau_seq β abv} (hf : ¬ lim_zero f) :
id                        └─────┘  └─┘         └──────┘ 
src                       └─────┘               └──────┘
typ                       └─────┘  └─┘         └──────┘ 
doc                                              └──────┘
453    ∀ ε > 0, ∃ i, ∀ j ≥ i, abv ((f j)⁻¹ - (f i)⁻¹) < ε | ε ε0 :=
id                      └─┘     └┘     └┘        └┘
src                                   └┘       └┘  
typ                     └─┘     └┘     └┘        └┘
454  let ⟨K, K0, HK⟩ := abv_pos_of_not_lim_zero hf,
id   └─┘     └┘  └┘     └─────────────────────┘ └┘
src                     └─────────────────────┘
typ  └─┘     └┘  └┘     └─────────────────────┘ └┘
455      ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abv ε0 K0,
id           └┘  └┘     └──────────────────────┘ └─┘
src                     └──────────────────────┘
typ          └┘  └┘     └──────────────────────┘ └─┘
456      ⟨i, H⟩ := exists_forall_ge_and HK (f.cauchy₃ δ0) in
id               └──────────────────┘     └──────┘
src                └──────────────────┘      └──────┘
typ              └──────────────────┘     └──────┘
457  ⟨i, λ j ij, let ⟨iK, H'⟩ := H _ (le_refl _) in Hδ (H _ ij).1 iK (H' _ ij)⟩
id          └┘  └─┘  └┘  └┘          └─────┘               └┘            └┘
src                                   └─────┘                  
typ         └┘  └─┘  └┘  └┘          └─────┘               └┘            └┘
458  
459  def inv (f) (hf : ¬ lim_zero f) : cau_seq β abv := ⟨_, inv_aux hf⟩
id                      └──────┘     └─────┘  └─┘        └─────┘ └┘
src                     └──────┘      └─────┘              └─────┘
typ                     └──────┘     └─────┘  └─┘        └─────┘ └┘
doc                      └──────┘
460  
461  @[simp] theorem inv_apply {f : cau_seq β abv} (hf i) : inv f hf i = (f i)⁻¹ := rfl
id                                  └─────┘  └─┘           └─┘  └┘      └┘    └─┘
src                                 └─────┘                 └─┘              └┘    └─┘
typ                                 └─────┘  └─┘           └─┘  └┘      └┘    └─┘
doc    └──┘
462  
463  theorem inv_mul_cancel {f : cau_seq β abv} (hf) : inv f hf * f ≈ 1 :=
id                               └─────┘  └─┘         └─┘  └┘   
src                              └─────┘               └─┘         
typ                              └─────┘  └─┘         └─┘  └┘   
464  λ ε ε0, let ⟨K, K0, i, H⟩ := abv_pos_of_not_lim_zero hf in
id      └┘  └─┘                 └─────────────────────┘ └┘
src                               └─────────────────────┘
typ     └┘  └─┘                 └─────────────────────┘ └┘
465  ⟨i, λ j ij,
id          └┘
typ         └┘
466    by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)),
id                └─────┘ └─┘     └────────────┘ └┘     └┘
src       └─────┘ └─────┘   └──┘ └────────────┘    └─┘  └───
typ       └─────┘ └─────┘└─┘└──┘ └────────────┘└┘ └─┘└┘└───
doc       └─────┘           └──┘                   └─┘  └───
txt       └─────┘           └──┘                   └─┘  └───
par       └─────┘           └──┘                   └─┘  └───
pid                       └──┘                   └─┘  └───
st       └─────────────────────────────────────────────────────
467      abv_zero abv] using ε0⟩
id       └──────┘ └─┘        └┘
src  ───┘└──────┘   └──────┘
typ  ───┘└──────┘└─┘└──────┘└┘
doc  ───┘           └──────┘
txt  ───┘           └──────┘
par  ───┘           └──────┘
pid  ───┘           └────┘
st   ─────────────────────────┘
468  
469  theorem const_inv {x : β} (hx : x ≠ 0) : const abv (x⁻¹) = inv (const abv x) (by rwa const_lim_zero) :=
id                                         └───┘ └─┘  └┘   └─┘  └───┘ └─┘           └────────────┘
src                                          └───┘       └┘   └─┘  └───┘            └──┘└────────────┘
typ                                        └───┘ └─┘  └┘   └─┘  └───┘ └─┘       └──┘└────────────┘
doc                                           └───┘                  └───┘            └──┘
txt                                                                                   └──┘
par                                                                                   └──┘
pid                                                                                      
st                                                                                   └─────────────────┘
470  ext (assume n, by simp[inv_apply, const_apply])
id   └─┘                   └───────┘  └─────────┘
src  └─┘               └───┘└───────┘└┘└─────────┘
typ  └─┘              └───┘└───────┘└┘└─────────┘
doc                    └───┘         └┘           
txt                    └───┘         └┘           
par                    └───┘         └┘           
pid                                 └┘           
st                    └───────────────────────────┘
471  
472  end discrete_field
473  
474  section abs
475  local notation `const` := const abs
id                             └───┘ └─┘
src                            └───┘ └─┘
typ                            └───┘ └─┘
doc                            └───┘
476  
477  /-- The entries of a positive Cauchy sequence eventually have a positive lower bound. -/
478  def pos (f : cau_seq α abs) : Prop := ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ f j
id                └─────┘  └─┘                              
src               └─────┘   └─┘                                 
typ               └─────┘  └─┘                              
479  
480  theorem not_lim_zero_of_pos {f : cau_seq α abs} : pos f → ¬ lim_zero f
id                                    └─────┘  └─┘    └─┘    └──────┘ 
src                                   └─────┘   └─┘    └─┘      └──────┘
typ                                   └─────┘  └─┘    └─┘    └──────┘ 
doc                                                    └─┘       └──────┘
481  | ⟨F, F0, hF⟩ H :=
id         └┘  └┘  
typ        └┘  └┘  
482    let ⟨i, h⟩ := exists_forall_ge_and hF (H _ F0),
id     └─┘          └──────────────────┘
src                  └──────────────────┘
typ    └─┘          └──────────────────┘
483        ⟨h₁, h₂⟩ := h _ (le_refl _) in
id          └┘  └┘          └─────┘
src                         └─────┘
typ         └┘  └┘          └─────┘
484    not_lt_of_le h₁ (abs_lt.1 h₂).2
id     └──────────┘     └────┘     
src    └──────────┘     └────┘     
typ    └──────────┘     └────┘     
485  
486  theorem const_pos {x : α} : pos (const x) ↔ 0 < x :=
id                              └─┘  └───┘       
src                              └─┘  └───┘       
typ                             └─┘  └───┘       
doc                              └─┘  └───┘
487  ⟨λ ⟨K, K0, i, h⟩, lt_of_lt_of_le K0 (h _ (le_refl _)),
id         └┘        └────────────┘          └─────┘
src                    └────────────┘          └─────┘
typ        └┘        └────────────┘          └─────┘
488   λ h, ⟨x, h, 0, λ j _, le_refl _⟩⟩
id                     └─────┘
src                         └─────┘
typ                    └─────┘
489  
490  theorem add_pos {f g : cau_seq α abs} : pos f → pos g → pos (f + g)
id                          └─────┘  └─┘    └─┘   └─┘    └─┘    
src                         └─────┘   └─┘    └─┘    └─┘     └─┘    
typ                         └─────┘  └─┘    └─┘   └─┘    └─┘    
doc                                          └─┘     └─┘     └─┘
491  | ⟨F, F0, hF⟩ ⟨G, G0, hG⟩ :=
id         └┘  └┘      └┘  └┘
typ        └┘  └┘      └┘  └┘
492    let ⟨i, h⟩ := exists_forall_ge_and hF hG in
id     └─┘         └──────────────────┘
src                  └──────────────────┘
typ    └─┘         └──────────────────┘
493    ⟨_, _root_.add_pos F0 G0, i,
id         └────────────┘
src        └────────────┘
typ        └────────────┘
494      λ j ij, let ⟨h₁, h₂⟩ := h _ ij in add_le_add h₁ h₂⟩
id          └┘  └─┘  └┘  └┘         └┘    └────────┘
src                                        └────────┘
typ         └┘  └─┘  └┘  └┘         └┘    └────────┘
495  
496  theorem pos_add_lim_zero {f g : cau_seq α abs} : pos f → lim_zero g → pos (f + g)
id                                   └─────┘  └─┘    └─┘   └──────┘    └─┘    
src                                  └─────┘   └─┘    └─┘     └──────┘     └─┘    
typ                                  └─────┘  └─┘    └─┘   └──────┘    └─┘    
doc                                                   └─┘     └──────┘     └─┘
497  | ⟨F, F0, hF⟩ H :=
id         └┘  └┘  
typ        └┘  └┘  
498    let ⟨i, h⟩ := exists_forall_ge_and hF (H _ (half_pos F0)) in
id     └─┘          └──────────────────┘          └──────┘
src                  └──────────────────┘          └──────┘
typ    └─┘          └──────────────────┘          └──────┘
499    ⟨_, half_pos F0, i, λ j ij, begin
id         └──────┘           └┘
src        └──────┘
typ        └──────┘           └┘
st                                 └─────
500      cases h j ij with h₁ h₂,
id               └┘
src      └────┘    └─────────┘
typ      └────┘└┘└─────────┘
doc      └────┘    └─────────┘
txt      └────┘    └─────────┘
par      └────┘    └─────────┘
pid               └─────────┘
st   ──────────────────────────┘└─
501      have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1),
id               └────────┘ └┘  └──────┘  └────┘   └┘
src      └──────┘└────────┘   └──────┘ └────┘└─┘  └──┘
typ      └──────┘└────────┘└┘ └──────┘ └────┘└─┘└┘└──┘
doc      └──────┘                            └─┘  └──┘
txt      └──────┘                            └─┘  └──┘
par      └──────┘                            └─┘  └──┘
pid      └───┘└─┘                            └─┘  └──┘
st   ───────────────────────────────────────────────────┘└─
502      rwa [← sub_eq_add_neg, sub_self_div_two] at this
id              └────────────┘  └──────────────┘
src      └─────┘└────────────┘└┘└──────────────┘└─────────
typ      └─────┘└────────────┘└┘└──────────────┘└─────────
doc      └─────┘              └┘                └─────────
txt      └─────┘              └┘                └─────────
par      └─────┘              └┘                └─────────
pid         └──┘              └┘                └──────┘
st   ────────────────────────┘└────────────────┘└────────
503    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
504  
505  theorem mul_pos {f g : cau_seq α abs} : pos f → pos g → pos (f * g)
id                          └─────┘  └─┘    └─┘   └─┘    └─┘    
src                         └─────┘   └─┘    └─┘    └─┘     └─┘    
typ                         └─────┘  └─┘    └─┘   └─┘    └─┘    
doc                                          └─┘     └─┘     └─┘
506  | ⟨F, F0, hF⟩ ⟨G, G0, hG⟩ :=
id         └┘  └┘      └┘  └┘
typ        └┘  └┘      └┘  └┘
507    let ⟨i, h⟩ := exists_forall_ge_and hF hG in
id     └─┘         └──────────────────┘
src                  └──────────────────┘
typ    └─┘         └──────────────────┘
508    ⟨_, _root_.mul_pos F0 G0, i,
id         └────────────┘
src        └────────────┘
typ        └────────────┘
509      λ j ij, let ⟨h₁, h₂⟩ := h _ ij in
id          └┘  └─┘  └┘  └┘         └┘
typ         └┘  └─┘  └┘  └┘         └┘
510      mul_le_mul h₁ h₂ (le_of_lt G0) (le_trans (le_of_lt F0) h₁)⟩
id       └────────┘        └──────┘      └──────┘  └──────┘
src      └────────┘        └──────┘      └──────┘  └──────┘
typ      └────────┘        └──────┘      └──────┘  └──────┘
511  
512  theorem trichotomy (f : cau_seq α abs) : pos f ∨ lim_zero f ∨ pos (-f) :=
id                           └─────┘  └─┘    └─┘   └──────┘   └─┘  
src                          └─────┘   └─┘    └─┘    └──────┘    └─┘  
typ                          └─────┘  └─┘    └─┘   └──────┘   └─┘  
doc                                           └─┘     └──────┘     └─┘
513  begin
st   └─────
514    cases classical.em (lim_zero f); simp *,
id           └──────────┘  └──────┘ 
src    └────┘└──────────┘ └──────┘   └────┘
typ    └────┘└──────────┘ └──────┘  └────┘
doc    └────┘             └──────┘   └────┘
txt    └────┘                        └────┘
par    └────┘                        └────┘
pid                                     
st   ────────────────────────────────────────┘└─
515    rcases abv_pos_of_not_lim_zero h with ⟨K, K0, hK⟩,
id            └─────────────────────┘ 
src    └─────┘└─────────────────────┘ └───────────────┘
typ    └─────┘└─────────────────────┘└───────────────┘
doc    └─────┘                        └───────────────┘
txt    └─────┘                        └───────────────┘
par    └─────┘                        └───────────────┘
pid                                  └───────────────┘
st   ──────────────────────────────────────────────────┘└─
516    rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩,
id            └──────────────────┘ └┘  └───────┘ └┘
src    └─────┘└──────────────────┘   └───────┘  └────────────┘
typ    └─────┘└──────────────────┘└┘ └───────┘└┘└────────────┘
doc    └─────┘                                  └────────────┘
txt    └─────┘                                  └────────────┘
par    └─────┘                                  └────────────┘
pid                                            └────────────┘
st   ───────────────────────────────────────────────────────────┘└─
517    refine (le_total 0 (f i)).imp _ _;
id             └──────┘     
src    └─────┘ └──────┘└─┘   └────────┘
typ    └─────┘ └──────┘└─┘ └────────┘
doc    └─────┘         └─┘   └────────┘
txt    └─────┘         └─┘   └────────┘
par    └─────┘         └─┘   └────────┘
pid                   └─┘   └────────┘
st   ─────────────────────────────────────
518      refine (λ h, ⟨K, K0, i, λ j ij, _⟩);
id                       └┘  
src      └─────┘  └──┘  └┘  └┘ └┘ └────────┘
typ      └─────┘  └──┘ └┘└┘└┘└┘ └────────┘
doc      └─────┘  └──┘  └┘  └┘ └┘ └────────┘
txt      └─────┘  └──┘  └┘  └┘ └┘ └────────┘
par      └─────┘  └──┘  └┘  └┘ └┘ └────────┘
pid              └──┘  └┘  └┘ └┘ └────────┘
st   ─────────────────────────────────────────
519      have := (hi _ ij).1;
id                └┘   └┘
src      └──────┘   └─┘  └─┘
typ      └──────┘ └┘└─┘└┘└─┘
doc      └──────┘   └─┘  └─┘
txt      └──────┘   └─┘  └─┘
par      └──────┘   └─┘  └─┘
pid      └───┘└─┘   └─┘  └┘
st   ─────────────────────────
520      cases hi _ (le_refl _) with h₁ h₂,
id             └┘    └─────┘
src      └────┘  └─┘ └─────┘└────────────┘
typ      └────┘└┘└─┘ └─────┘└────────────┘
doc      └────┘  └─┘        └────────────┘
txt      └────┘  └─┘        └────────────┘
par      └────┘  └─┘        └────────────┘
pid             └─┘        └─┘└─────────┘
st   ────────────────────────────────────┘└─
521    { rwa abs_of_nonneg at this,
id           └───────────┘
src      └──┘└───────────┘└──────┘
typ      └──┘└───────────┘└──────┘
doc      └──┘             └──────┘
txt      └──┘             └──────┘
par      └──┘             └──────┘
pid                      └──────┘
st   ───┘└───────────────────────┘└─
522      rw abs_of_nonneg h at h₁,
id          └───────────┘ 
src      └─┘└───────────┘ └────┘
typ      └─┘└───────────┘└────┘
doc      └─┘              └────┘
txt      └─┘              └────┘
par      └─┘              └────┘
pid                      └────┘
st   ───────────────────────────┘└─
523      exact (le_add_iff_nonneg_right _).1
id              └─────────────────────┘
src      └────┘ └─────────────────────┘└─────
typ      └────┘ └─────────────────────┘└─────
doc      └────┘                        └─────
txt      └────┘                        └─────
par      └────┘                        └─────
pid                                   └─────
st   ────────────────────────────────────────
524        (le_trans h₁ $ neg_le_sub_iff_le_add'.1 $
id          └──────┘ └┘   └────────────────────┘
src  ─────┘ └──────┘   └────────────────────┘└─┘ 
typ  ─────┘ └──────┘└┘ └────────────────────┘└─┘ 
doc  ─────┘                                  └─┘ 
txt  ─────┘                                  └─┘ 
par  ─────┘                                  └─┘ 
pid  ─────┘                                  └─┘ 
st   ────────────────────────────────────────────────
525          le_of_lt (abs_lt.1 $ h₂ _ ij).1) },
id           └──────┘  └────┘     └┘   └┘
src  ───────┘└──────┘ └────┘└─┘   └─┘  └───┘
typ  ───────┘└──────┘ └────┘└─┘ └┘└─┘└┘└───┘
doc  ───────┘               └─┘   └─┘  └───┘
txt  ───────┘               └─┘   └─┘  └───┘
par  ───────┘               └─┘   └─┘  └───┘
pid  ───────┘               └─┘   └─┘  └──┘
st   ────────────────────────────────────────┘└┘
526    { rwa abs_of_nonpos at this,
id           └───────────┘
src      └──┘└───────────┘└──────┘
typ      └──┘└───────────┘└──────┘
doc      └──┘             └──────┘
txt      └──┘             └──────┘
par      └──┘             └──────┘
pid                      └──────┘
st   ────────────────────────────┘└─
527      rw abs_of_nonpos h at h₁,
id          └───────────┘ 
src      └─┘└───────────┘ └────┘
typ      └─┘└───────────┘└────┘
doc      └─┘              └────┘
txt      └─┘              └────┘
par      └─┘              └────┘
pid                      └────┘
st   ───────────────────────────┘└─
528      rw [← sub_le_sub_iff_right, zero_sub],
id             └──────────────────┘  └──────┘
src      └────┘└──────────────────┘└┘└──────┘
typ      └────┘└──────────────────┘└┘└──────┘
doc      └────┘                    └┘        
txt      └────┘                    └┘        
par      └────┘                    └┘        
pid        └──┘                    └┘        
st   ─────────────────────────────┘└────────┘└──
529      exact le_trans (le_of_lt (abs_lt.1 $ h₂ _ ij).2) h₁ }
id             └──────┘  └──────┘  └────┘     └┘   └┘     └┘
src      └────┘└──────┘ └──────┘ └────┘└─┘   └─┘  └───┘  
typ      └────┘└──────┘ └──────┘ └────┘└─┘ └┘└─┘└┘└───┘└┘
doc      └────┘                        └─┘   └─┘  └───┘  
txt      └────┘                        └─┘   └─┘  └───┘  
par      └────┘                        └─┘   └─┘  └───┘  
pid                                   └─┘   └─┘  └───┘  
st   ───────────────────────────────────────────────────────┘└─
530  end
st   ──┘
531  
532  instance : has_lt (cau_seq α abs) := ⟨λ f g, pos (g - f)⟩
id              └────┘  └─────┘  └─┘           └─┘    
src             └────┘  └─────┘   └─┘             └─┘    
typ             └────┘  └─────┘  └─┘           └─┘    
doc                                               └─┘
533  instance : has_le (cau_seq α abs) := ⟨λ f g, f < g ∨ f ≈ g⟩
id              └────┘  └─────┘  └─┘                 
src             └────┘  └─────┘   └─┘                     
typ             └────┘  └─────┘  └─┘                 
534  
535  theorem lt_of_lt_of_eq {f g h : cau_seq α abs}
id                                   └─────┘  └─┘
src                                  └─────┘   └─┘
typ                                  └─────┘  └─┘
536    (fg : f < g) (gh : g ≈ h) : f < h :=
id                             
src                                
typ                            
537  by simpa using pos_add_lim_zero fg (neg_lim_zero gh)
id                  └──────────────┘ └┘  └──────────┘ └┘
src     └──────────┘└──────────────┘   └──────────┘  └─
typ     └──────────┘└──────────────┘└┘ └──────────┘└┘└─
doc     └──────────┘                                 └─
txt     └──────────┘                                 └─
par     └──────────┘                                 └─
pid          └────┘                                 
st     └──────────────────────────────────────────────────
538  
src  
typ  
doc  
txt  
par  
pid  
st   
539  theorem lt_of_eq_of_lt {f g h : cau_seq α abs}
id                                   └─────┘  └─┘
src                                  └─────┘   └─┘
typ                                  └─────┘  └─┘
540    (fg : f ≈ g) (gh : g < h) : f < h :=
id                             
src                                
typ                            
541  by have := pos_add_lim_zero gh (neg_lim_zero fg);
id              └──────────────┘ └┘  └──────────┘ └┘
src     └──────┘└──────────────┘   └──────────┘  
typ     └──────┘└──────────────┘└┘ └──────────┘└┘
doc     └──────┘                                 
txt     └──────┘                                 
par     └──────┘                                 
pid     └───┘└─┘                                 
st     └───────────────────────────────────────────────
542     rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this
id             └────────────┘  └──────────────────────┘
src     └─────┘└────────────┘└┘└──────────────────────┘└─────────
typ     └─────┘└────────────┘└┘└──────────────────────┘└─────────
doc     └─────┘              └┘                        └─────────
txt     └─────┘              └┘                        └─────────
par     └─────┘              └┘                        └─────────
pid        └──┘              └┘                        └──────┘
st   ───────┘└──────────────┘└────────────────────────┘└────────
543  
src  
typ  
doc  
txt  
par  
pid  
st   
544  theorem lt_trans {f g h : cau_seq α abs} (fg : f < g) (gh : g < h) : f < h :=
id                             └─────┘  └─┘                          
src                            └─────┘   └─┘                              
typ                            └─────┘  └─┘                          
545  by simpa using add_pos fg gh
id                  └─────┘ └┘ └┘
src     └──────────┘└─────┘    
typ     └──────────┘└─────┘└┘└┘
doc     └──────────┘           
txt     └──────────┘           
par     └──────────┘           
pid          └────┘           
st     └──────────────────────────
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  theorem lt_irrefl {f : cau_seq α abs} : ¬ f < f
id                          └─────┘  └─┘       
src                         └─────┘   └─┘       
typ                         └─────┘  └─┘       
548  | h := not_lim_zero_of_pos h (by simp [zero_lim_zero])
id         └─────────────────┘             └───────────┘
src         └─────────────────┘       └────┘└───────────┘
typ        └─────────────────┘       └────┘└───────────┘
doc                                   └────┘             
txt                                   └────┘             
par                                   └────┘             
pid                                                    
st                                   └───────────────────┘
549  
550  lemma le_of_eq_of_le {f g h : cau_seq α abs}
id                                 └─────┘  └─┘
src                                └─────┘   └─┘
typ                                └─────┘  └─┘
551    (hfg : f ≈ g) (hgh : g ≤ h) : f ≤ h :=
id                               
src                                  
typ                              
552  hgh.elim (or.inl ∘ cau_seq.lt_of_eq_of_lt hfg)
id   └─┘└───┘  └────┘  └────────────────────┘ └─┘
src     └───┘  └────┘  └────────────────────┘
typ  └─┘└───┘  └────┘  └────────────────────┘ └─┘
553    (or.inr ∘ setoid.trans hfg)
id      └────┘  └──────────┘ └─┘
src     └────┘  └──────────┘
typ     └────┘  └──────────┘ └─┘
554  
555  lemma le_of_le_of_eq {f g h : cau_seq α abs}
id                                 └─────┘  └─┘
src                                └─────┘   └─┘
typ                                └─────┘  └─┘
556    (hfg : f ≤ g) (hgh : g ≈ h) : f ≤ h :=
id                               
src                                  
typ                              
557  hfg.elim (λ h, or.inl (cau_seq.lt_of_lt_of_eq h hgh))
id   └─┘└───┘      └────┘  └────────────────────┘  └─┘
src     └───┘       └────┘  └────────────────────┘
typ  └─┘└───┘      └────┘  └────────────────────┘  └─┘
558    (λ h, or.inr (setoid.trans h hgh))
id          └────┘  └──────────┘  └─┘
src          └────┘  └──────────┘
typ         └────┘  └──────────┘  └─┘
559  
560  instance : preorder (cau_seq α abs) :=
id              └──────┘  └─────┘  └─┘
src             └──────┘  └─────┘   └─┘
typ             └──────┘  └─────┘  └─┘
561  { lt := (<),
id           
src          
typ          
562    le := λ f g, f < g ∨ f ≈ g,
id                      
src                         
typ                     
563    le_refl := λ f, or.inr (setoid.refl _),
id                    └────┘  └─────────┘
src                    └────┘  └─────────┘
typ                   └────┘  └─────────┘
564    le_trans := λ f g h fg, match fg with
id                      └┘        └┘
typ                     └┘        └┘
565      | or.inl fg, or.inl gh := or.inl $ lt_trans fg gh
id                └┘  └────┘ └┘    └────┘   └──────┘
src                   └────┘       └────┘   └──────┘
typ               └┘  └────┘ └┘    └────┘   └──────┘
566      | or.inl fg, or.inr gh := or.inl $ lt_of_lt_of_eq fg gh
id         └────┘ └┘  └────┘ └┘    └────┘   └────────────┘
src        └────┘     └────┘       └────┘   └────────────┘
typ        └────┘ └┘  └────┘ └┘    └────┘   └────────────┘
567      | or.inr fg, or.inl gh := or.inl $ lt_of_eq_of_lt fg gh
id         └────┘ └┘  └────┘ └┘    └────┘   └────────────┘
src        └────┘     └────┘       └────┘   └────────────┘
typ        └────┘ └┘  └────┘ └┘    └────┘   └────────────┘
568      | or.inr fg, or.inr gh := or.inr $ setoid.trans fg gh
id                └┘  └────┘ └┘    └────┘   └──────────┘
src                   └────┘       └────┘   └──────────┘
typ               └┘  └────┘ └┘    └────┘   └──────────┘
569      end,
570    lt_iff_le_not_le := λ f g,
id                            
typ                           
571      ⟨λ h, ⟨or.inl h,
id             └────┘ 
src             └────┘
typ            └────┘ 
572        not_or (mt (lt_trans h) lt_irrefl) (not_lim_zero_of_pos h)⟩,
id         └────┘  └┘  └──────┘   └───────┘   └─────────────────┘ 
src        └────┘  └┘  └──────┘    └───────┘   └─────────────────┘
typ        └────┘  └┘  └──────┘   └───────┘   └─────────────────┘ 
573      λ ⟨h₁, h₂⟩, h₁.resolve_right
id         └┘  └┘     └────────────┘
src                    └────────────┘
typ        └┘  └┘     └────────────┘
574        (mt (λ h, or.inr (setoid.symm h)) h₂)⟩ }
id          └┘      └────┘  └─────────┘ 
src         └┘       └────┘  └─────────┘
typ         └┘      └────┘  └─────────┘ 
575  
576  theorem le_antisymm {f g : cau_seq α abs} (fg : f ≤ g) (gf : g ≤ f) : f ≈ g :=
id                              └─────┘  └─┘                          
src                             └─────┘   └─┘                              
typ                             └─────┘  └─┘                          
577  fg.resolve_left (not_lt_of_le gf)
id   └┘└───────────┘  └──────────┘ └┘
src    └───────────┘  └──────────┘
typ  └┘└───────────┘  └──────────┘ └┘
578  
579  theorem lt_total (f g : cau_seq α abs) : f < g ∨ f ≈ g ∨ g < f :=
id                           └─────┘  └─┘              
src                          └─────┘   └─┘                  
typ                          └─────┘  └─┘              
580  (trichotomy (g - f)).imp_right
id    └────────┘      └───────┘
src   └────────┘        └───────┘
typ   └────────┘      └───────┘
581    (λ h, h.imp (λ h, setoid.symm h) (λ h, by rwa neg_sub at h))
id          └──┘      └─────────┘               └─────┘
src           └──┘       └─────────┘             └──┘└─────┘└───┘
typ         └──┘      └─────────┘           └──┘└─────┘└───┘
doc                                              └──┘       └───┘
txt                                              └──┘       └───┘
par                                              └──┘       └───┘
pid                                                        └───┘
st                                              └───────────────┘
582  
583  theorem le_total (f g : cau_seq α abs) : f ≤ g ∨ g ≤ f :=
id                           └─────┘  └─┘          
src                          └─────┘   └─┘            
typ                          └─────┘  └─┘          
584  (or.assoc.2 (lt_total f g)).imp_right or.inl
id    └──────┘   └──────┘    └───────┘  └────┘
src   └──────┘   └──────┘      └───────┘  └────┘
typ   └──────┘   └──────┘    └───────┘  └────┘
585  
586  theorem const_lt {x y : α} : const x < const y ↔ x < y :=
id                               └───┘   └───┘     
src                               └───┘    └───┘      
typ                              └───┘   └───┘     
doc                               └───┘     └───┘
587  show pos _ ↔ _, by rw [← const_sub, const_pos, sub_pos]
id        └─┘                └───────┘  └───────┘  └─────┘
src       └─┘          └────┘└───────┘└┘└───────┘└┘└─────┘└─
typ       └─┘          └────┘└───────┘└┘└───────┘└┘└─────┘└─
doc       └─┘           └────┘         └┘         └┘       └─
txt                     └────┘         └┘         └┘       └─
par                     └────┘         └┘         └┘       └─
pid                       └──┘         └┘         └┘       
st                     └──────────────┘└─────────┘└───────┘
588  
src  
typ  
doc  
txt  
par  
pid  
st   
589  theorem const_le {x y : α} : const x ≤ const y ↔ x ≤ y :=
id                               └───┘   └───┘     
src                               └───┘    └───┘      
typ                              └───┘   └───┘     
doc                               └───┘     └───┘
590  by rw le_iff_lt_or_eq; exact or_congr const_lt const_equiv
id         └─────────────┘        └──────┘ └──────┘ └─────────┘
src     └─┘└─────────────┘  └────┘└──────┘└──────┘└─────────┘
typ     └─┘└─────────────┘  └────┘└──────┘└──────┘└─────────┘
doc     └─┘                 └────┘                           
txt     └─┘                 └────┘                           
par     └─┘                 └────┘                           
pid                                                        
st     └────────────────────────────────────────────────────────
591  
src  
typ  
doc  
txt  
par  
pid  
st   
592  lemma le_of_exists {f g : cau_seq α abs}
id                             └─────┘  └─┘
src                            └─────┘   └─┘
typ                            └─────┘  └─┘
593    (h : ∃ i, ∀ j ≥ i, f j ≤ g j) : f ≤ g :=
id                             
src                                   
typ                            
594  let ⟨i, hi⟩ := h in
id   └─┘    └┘     
typ  └─┘    └┘     
595  (or.assoc.2 (cau_seq.lt_total f g)).elim
id    └──────┘   └──────────────┘    └──┘
src   └──────┘   └──────────────┘      └──┘
typ   └──────┘   └──────────────┘    └──┘
596    id
id     └┘
src    └┘
typ    └┘
597    (λ hgf, false.elim (let ⟨K, hK0, j, hKj⟩ := hgf in
id        └─┘  └────────┘  └─┘     └─┘    └─┘     └─┘
src            └────────┘
typ       └─┘  └────────┘  └─┘     └─┘    └─┘     └─┘
598      not_lt_of_ge (hi (max i j) (le_max_left _ _))
id       └──────────┘      └─┘       └─────────┘
src      └──────────┘      └─┘       └─────────┘
typ      └──────────┘      └─┘       └─────────┘
599        (sub_pos.1 (lt_of_lt_of_le hK0 (hKj _ (le_max_right _ _))))))
id          └─────┘   └────────────┘             └──────────┘
src         └─────┘   └────────────┘             └──────────┘
typ         └─────┘   └────────────┘             └──────────┘
600  
601  theorem exists_gt (f : cau_seq α abs) : ∃ a : α, f < const a :=
id                          └─────┘  └─┘            └───┘ 
src                         └─────┘   └─┘              └───┘
typ                         └─────┘  └─┘            └───┘ 
doc                                                       └───┘
602  let ⟨K, H⟩ := f.bounded in
id   └─┘          └──────┘
src                 └──────┘
typ  └─┘          └──────┘
603  ⟨K + 1, 1, zero_lt_one, 0, λ i _, begin
id             └─────────┘        
src            └─────────┘
typ            └─────────┘        
st                                     └─────
604    rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right],
id         └───────┘  └─────────┘  └────────────────┘  └──────────────────┘
src    └──┘└───────┘└┘└─────────┘└┘└────────────────┘└┘└──────────────────┘
typ    └──┘└───────┘└┘└─────────┘└┘└────────────────┘└┘└──────────────────┘
doc    └──┘         └┘           └┘                  └┘                    
txt    └──┘         └┘           └┘                  └┘                    
par    └──┘         └┘           └┘                  └┘                    
pid      └┘         └┘           └┘                  └┘                    
st   ──────────────┘└───────────┘└──────────────────┘└────────────────────┘└──
605    exact le_of_lt (abs_lt.1 (H _)).2
id           └──────┘  └────┘    
src    └────┘└──────┘ └────┘└─┘  └─────┘
typ    └────┘└──────┘ └────┘└─┘ └─────┘
doc    └────┘               └─┘  └─────┘
txt    └────┘               └─┘  └─────┘
par    └────┘               └─┘  └─────┘
pid                        └─┘  └──┘└─┘
st   ───────────────────────────────────┘
606  end⟩
st   └─┘
607  
608  theorem exists_lt (f : cau_seq α abs) : ∃ a : α, const a < f :=
id                          └─────┘  └─┘          └───┘   
src                         └─────┘   └─┘           └───┘   
typ                         └─────┘  └─┘          └───┘   
doc                                                   └───┘
609  let ⟨a, h⟩ := (-f).exists_gt in ⟨-a, show pos _,
id   └─┘            └───────┘              └─┘
src                   └───────┘              └─┘
typ  └─┘            └───────┘              └─┘
doc                                            └─┘
610    by rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]⟩
id             └───────┘  └────────────┘  └──────┘    └────────────┘
src       └───┘└───────┘└┘└────────────┘└┘└──────┘└──┘└────────────┘
typ       └───┘└───────┘└┘└────────────┘└┘└──────┘└──┘└────────────┘
doc       └───┘         └┘              └┘        └──┘              
txt       └───┘         └┘              └┘        └──┘              
par       └───┘         └┘              └┘        └──┘              
pid          └┘         └┘              └┘        └──┘              
st       └─────────────┘└──────────────┘└────────┘└────────────────┘
611  
612  end abs
613  
614  end cau_seq